theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_eq_of_common_suffix {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (t u : P.RelationSurvivingSupport r) {y : Q} (s : Quiver.Path y z) (hs : s.length ≠ 0) (g h : Quiver.Path x y) (ht : ↑t = g.comp s) (hu : ↑u = h.comp s) : t = u

Two surviving arms of one relation which have a common nonempty suffix are the same arm.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_eq_of_common_prefix {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (t u : P.RelationSurvivingSupport r) {y : Q} (s : Quiver.Path x y) (hs : s.length ≠ 0) (g h : Quiver.Path y z) (ht : ↑t = s.comp g) (hu : ↑u = s.comp h) : t = u

Two surviving arms of one relation which have a common nonempty prefix are the same arm.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_path_coefficient_ne_zero_of_quotientMap_ne_zero {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (R : RelationFamily k Q) {x z : Q} (f : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hf : (LinearPathCategory.HomogeneousQuotient.quotientFunctor R).map f ≠ 0) : ∃ (p : Quiver.Path x z), ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) f) p ≠ 0 ∧ pathMap R p ≠ 0

A free morphism with nonzero image in a relation quotient has a basis path with both nonzero coefficient and nonzero quotient image.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientMap_eq_pathMap_sum {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (R : RelationFamily k Q) {x z : Q} (f : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) : (LinearPathCategory.HomogeneousQuotient.quotientFunctor R).map f = ∑ q ∈ ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) f).support, ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) f) q • pathMap R q

Mapping a free morphism to the relation quotient is the finite sum of its path coefficients times the corresponding path classes.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftPathExtensionLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x y z : Q} (g : Quiver.Path x y) : (LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q y) →ₗ[k] obj P.relations z ⟶ obj P.relations x

Extend a free linear combination of paths on the initial side by an arbitrary nonempty path and then pass to the special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.homPathCoefficient_eq_zero_of_leftPathExtension_eq_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x y z : Q} (g : Quiver.Path x y) (hg : g.length ≠ 0) (f : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q y) (hf : (P.leftPathExtensionLinearMap g) f = 0) (p : Quiver.Path y z) (hp : CategoryTheory.CategoryStruct.comp (pathMap P.relations p) (pathMap P.relations g) ≠ 0) : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q y)) f) p = 0

If extension by a nonempty initial path kills a free linear combination, then every coefficient whose extended path survives was already zero.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightPathExtensionLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x y z : Q} (h : Quiver.Path y z) : (LinearPathCategory.obj k Q y ⟶ LinearPathCategory.obj k Q x) →ₗ[k] obj P.relations z ⟶ obj P.relations x

Extend a free linear combination of paths on the terminal side by an arbitrary nonempty path and then pass to the special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.homPathCoefficient_eq_zero_of_rightPathExtension_eq_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x y z : Q} (h : Quiver.Path y z) (hh : h.length ≠ 0) (g : LinearPathCategory.obj k Q y ⟶ LinearPathCategory.obj k Q x) (hg : (P.rightPathExtensionLinearMap h) g = 0) (q : Quiver.Path x y) (hq : CategoryTheory.CategoryStruct.comp (pathMap P.relations h) (pathMap P.relations q) ≠ 0) : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)) g) q = 0

If extension by a nonempty terminal path kills a free linear combination, then every coefficient whose extended path survives was already zero.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.endingRelationSupportFactor {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations y z) : P.RelationSurvivingSupport r

The chosen maximal relation arm containing a surviving suffix.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.endingRelationComplement {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations y z) : Quiver.Path x y

The chosen complementary prefix from x to the initial vertex of a surviving suffix.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.endingRelationSupportFactor_path_eq {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations y z) : ↑(P.endingRelationSupportFactor r hr p s) = (P.endingRelationComplement r hr p s).comp ↑s

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.startingRelationSupportFactor {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations x y) : P.RelationSurvivingSupport r

The chosen maximal relation arm containing a surviving prefix.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.startingRelationComplement {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations x y) : Quiver.Path y z

The chosen complementary suffix from the terminal vertex of a surviving prefix to the terminal relation vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.startingRelationSupportFactor_path_eq {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (s : SurvivingPath P.relations x y) : ↑(P.startingRelationSupportFactor r hr p s) = (↑s).comp (P.startingRelationComplement r hr p s)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_comp_mem_relationEndpointLine_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (f : obj P.relations z ⟶ obj P.relations y) (hf : f ≠ 0) : ∃ (g : obj P.relations y ⟶ obj P.relations x), CategoryTheory.CategoryStruct.comp f g ∈ k ∙ pathMap P.relations ↑p ∧ CategoryTheory.CategoryStruct.comp f g ≠ 0

Every nonzero element of the terminal representable can be composed into the nonzero endpoint line of the paired relation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_left_comp_mem_relationEndpointLine_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) {y : Q} (g : obj P.relations y ⟶ obj P.relations x) (hg : g ≠ 0) : ∃ (f : obj P.relations z ⟶ obj P.relations y), CategoryTheory.CategoryStruct.comp f g ∈ k ∙ pathMap P.relations ↑p ∧ CategoryTheory.CategoryStruct.comp f g ≠ 0

Every nonzero element of the initial representable can be composed into the nonzero endpoint line of the paired relation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFunctional_ne_zero_of_mem_span {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) (h : obj P.relations z ⟶ obj P.relations x) (hmem : h ∈ k ∙ pathMap P.relations ↑p) (hne : h ≠ 0) : (P.relationSurvivingSupportFunctional r hr p) h ≠ 0

The normalized endpoint functional is nonzero on every nonzero element of the relation endpoint line.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportTransposeLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) (Y : Category P.relations) : (Y ⟶ obj P.relations x) →ₗ[k] Module.Dual k (obj P.relations z ⟶ Y)

The transpose of the relation composition pairing at one displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportTransposeLinearMap_apply_apply {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) (Y : Category P.relations) (g : Y ⟶ obj P.relations x) (f : obj P.relations z ⟶ Y) : ((P.relationSurvivingSupportTransposeLinearMap r hr p Y) g) f = (P.relationSurvivingSupportFunctional r hr p) (CategoryTheory.CategoryStruct.comp f g)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.hasPerfectRelationPairing {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) : P.HasPerfectRelationPairing r hr p

The composition pairing induced by a surviving relation arm is perfect.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportNakayamaHom_isIso_of_specialBiserial {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) : CategoryTheory.IsIso (P.relationSurvivingSupportNakayamaHom r hr p)

The relation-induced Nakayama map is unconditionally an isomorphism for a special-biserial presentation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSourceRepresentable_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) : CategoryTheory.Injective (P.relationSourceRepresentable z)

The representable ending at a surviving special-biserial relation arm is injective.