Linear independence along a special-biserial branch

The unique-continuation condition orders the surviving paths beginning with one fixed arrow by length. Even when the presentation is not monomial, the images of those paths with a fixed endpoint are linearly independent. The key point is that a relation with a shortest nonzero coefficient factors as a nonzero scalar plus a positive-tail endomorphism; admissibility makes the positive part nilpotent, hence the factor is invertible.

theorem Module.Basis.repr_eq_zero_of_map_eq_zero_of_image_ne_zero {k : Type u₁} [Field k] {I : Type u₂} {V : Type u₃} {W : Type u₄} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (b : Basis I k V) (f : V →ₗ[k] W) (hli : LinearIndependent k fun (i : { i : I // f (b i) ≠ 0 }) => f (b ↑i)) (v : V) (hv : f v = 0) (i : I) (hi : f (b i) ≠ 0) : (b.repr v) i = 0

If the nonzero images of basis vectors are linearly independent, a vector killed by the linear map has zero coefficient at every basis vector whose image is nonzero.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightBranchPathMap {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 : Q} (a : x ⟶ y) (z : Q) (q : P.RightContinuationAt a z) : obj P.relations z ⟶ obj P.relations x

The quotient morphism represented by a surviving continuation followed by its fixed initial arrow.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightBranchPathMap_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 y : Q} (a : x ⟶ y) (z : Q) (q : P.RightContinuationAt a z) : P.rightBranchPathMap a z q ≠ 0

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightBranchPathMap_eq_factor_comp {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 : Q} (a : x ⟶ y) (z : Q) (p q : P.RightContinuationAt a z) (r : Quiver.Path z z) (hr : ↑q = (↑p).comp r) : P.rightBranchPathMap a z q = CategoryTheory.CategoryStruct.comp (pathMap P.relations r) (P.rightBranchPathMap a z p)

Factoring a continuation path factors the corresponding branch morphism on the left.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathMap_mem_quotientHomLengthTail_one_of_length_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) (z : Q) (r : Quiver.Path z z) (hr : r.length ≠ 0) : pathMap P.relations r ∈ ⋯.quotientHomLengthTail (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q z) 1

A positive-length loop maps into the positive part of the admissible path filtration.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightBranchPathMap_linearIndependent {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 : Q} (a : x ⟶ y) (z : Q) : LinearIndependent k (P.rightBranchPathMap a z)

Distinct surviving paths in one fixed special-biserial branch remain linearly independent in the original (possibly nonmonomial) quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftBranchPathMap {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 : Q} (a : x ⟶ y) (z : Q) (p : P.LeftContinuationAt a z) : obj P.relations y ⟶ obj P.relations z

The quotient morphism represented by a fixed final arrow preceded by a surviving left continuation.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftBranchPathMap_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 y : Q} (a : x ⟶ y) (z : Q) (p : P.LeftContinuationAt a z) : P.leftBranchPathMap a z p ≠ 0

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftBranchPathMap_eq_comp_factor {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 : Q} (a : x ⟶ y) (z : Q) (p q : P.LeftContinuationAt a z) (r : Quiver.Path z z) (hr : ↑q = r.comp ↑p) : P.leftBranchPathMap a z q = CategoryTheory.CategoryStruct.comp (P.leftBranchPathMap a z p) (pathMap P.relations r)

Factoring a left continuation path factors the corresponding branch morphism on the right.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftBranchPathMap_linearIndependent {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 : Q} (a : x ⟶ y) (z : Q) : LinearIndependent k (P.leftBranchPathMap a z)

Distinct surviving paths in one fixed left branch remain linearly independent in the original (possibly nonmonomial) quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightExtensionLinearMap {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 w : Q} (b : z ⟶ w) : (LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) →ₗ[k] obj P.relations w ⟶ obj P.relations x

Extend a free linear combination of paths on the right by one displayed arrow and then pass to the relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftExtensionLinearMap {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) {w x z : Q} (c : w ⟶ x) : (LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) →ₗ[k] obj P.relations z ⟶ obj P.relations w

Extend a free linear combination of paths on the left by one displayed arrow and then pass to the relation quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.homPathCoefficient_eq_zero_of_rightExtension_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 z w : Q} (b : z ⟶ w) (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : (P.rightExtensionLinearMap b) r = 0) (p : Quiver.Path x z) (hp : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (pathMap P.relations p) ≠ 0) : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) p = 0

If right extension of a linear relation vanishes, then every path which survives that extension has zero coefficient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.homPathCoefficient_eq_zero_of_leftExtension_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) {w x z : Q} (c : w ⟶ x) (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : (P.leftExtensionLinearMap c) r = 0) (p : Quiver.Path x z) (hp : CategoryTheory.CategoryStruct.comp (pathMap P.relations p) (arrowMap P.relations c) ≠ 0) : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) p = 0

If left extension of a linear relation vanishes, then every path which survives that extension has zero coefficient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSupportPath_rightExtension_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 z w : 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 : Quiver.Path x z) (hp : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) p ≠ 0) (b : z ⟶ w) : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (pathMap P.relations p) = 0

Every surviving path occurring in a displayed special-biserial relation is right-maximal: adjoining any arrow at its endpoint kills it.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSupportPath_leftExtension_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) {w 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 : Quiver.Path x z) (hp : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) p ≠ 0) (c : w ⟶ x) : CategoryTheory.CategoryStruct.comp (pathMap P.relations p) (arrowMap P.relations c) = 0

Every surviving path occurring in a displayed special-biserial relation is left-maximal: adjoining any arrow at its source kills it.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullGenerator_rightExtension_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 : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) {w : Q} (b : LinearPathCategory.vertex X ⟶ w) : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) = 0

Every generator of the path-support hull is right-maximal already in the original special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullGenerator_leftExtension_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 : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) {w : Q} (c : w ⟶ LinearPathCategory.vertex Y) : CategoryTheory.CategoryStruct.comp ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) (arrowMap P.relations c) = 0

Every generator of the path-support hull is left-maximal already in the original special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathMap_comp_pathSupportHullGenerator_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 : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) {w : Q} (q : Quiver.Path (LinearPathCategory.vertex X) w) (hq : q.length ≠ 0) : CategoryTheory.CategoryStruct.comp (pathMap P.relations q) ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) = 0

A nonempty path on the right of a path-support-hull generator kills that generator in the original quotient. Here "right" refers to the displayed quiver direction; it is precomposition categorically.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullGenerator_comp_pathMap_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 : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) {w : Q} (q : Quiver.Path w (LinearPathCategory.vertex Y)) (hq : q.length ≠ 0) : CategoryTheory.CategoryStruct.comp ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) (pathMap P.relations q) = 0

A nonempty path on the left of a path-support-hull generator kills that generator in the original quotient. Here "left" refers to the displayed quiver direction; it is postcomposition categorically.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientMap_comp_pathSupportHullGenerator_eq_zero_of_mem_lengthTail_one {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) {W X Y : LinearPathCategory.Category k Q} (g : W ⟶ X) (hg : g ∈ LinearPathCategory.lengthTail W X 1) {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) : CategoryTheory.CategoryStruct.comp ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map g) ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) = 0

A positive free morphism precomposed with a path-support-hull generator maps to zero in the original quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullGenerator_comp_quotientMap_eq_zero_of_mem_lengthTail_one {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 : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hf : f ∈ pathSupportHull P.relations X Y) (g : Y ⟶ Z) (hg : g ∈ LinearPathCategory.lengthTail Y Z 1) : CategoryTheory.CategoryStruct.comp ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map g) = 0

A path-support-hull generator postcomposed with a positive free morphism maps to zero in the original quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullIdeal_rightExtension_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 : LinearPathCategory.Category k Q} (f : X ⟶ Y) (hf : f ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (pathSupportHull P.relations) X Y) {w : Q} (b : LinearPathCategory.vertex X ⟶ w) : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) = 0

Every element of the two-sided ideal generated by the path-support hull is killed by precomposition with a displayed arrow after mapping back to the original special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullIdeal_leftExtension_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 : LinearPathCategory.Category k Q} (f : X ⟶ Y) (hf : f ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (pathSupportHull P.relations) X Y) {w : Q} (b : w ⟶ LinearPathCategory.vertex Y) : CategoryTheory.CategoryStruct.comp ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f) (arrowMap P.relations b) = 0

Every element of the two-sided ideal generated by the path-support hull is killed by postcomposition with a displayed arrow after mapping back to the original special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_rightExtension_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 : Category P.relations} (f : X ⟶ Y) (hf : f ∈ (relativeRelationHomIdeal ⋯).hom X Y) {w : Q} (b : LinearPathCategory.vertex X.as ⟶ w) : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) f = 0

A morphism in the relative path-support-hull kernel is annihilated on the right by every displayed arrow in the original quotient category.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_leftExtension_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 : Category P.relations} (f : X ⟶ Y) (hf : f ∈ (relativeRelationHomIdeal ⋯).hom X Y) {w : Q} (b : w ⟶ LinearPathCategory.vertex Y.as) : CategoryTheory.CategoryStruct.comp f (arrowMap P.relations b) = 0

A morphism in the relative path-support-hull kernel is annihilated on the left by every displayed arrow in the original quotient category.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.RelationSurvivingSupport {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) : Type u

The paths in a displayed relation which still survive in the original special-biserial quotient.

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.InitialDecomposition {Q : Type u} [Quiver Q] {x z : Q} (p : Quiver.Path x z) : Type u

A nonempty path decomposed into its first arrow and remaining tail.

• middle : Q
• arrow : x ⟶ self.middle
• tail : Quiver.Path self.middle z
• path_eq : p = self.arrow.toPath.comp self.tail
• length_eq : p.length = self.tail.length + 1

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_length_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) : (↑p).length ≠ 0

Every path in the surviving support of a displayed relation has length at least two, hence in particular has a first arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportInitialDecomposition {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) : InitialDecomposition ↑p

A chosen first-arrow decomposition for a surviving relation-support path.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportInitialArrow {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.RelationSurvivingSupport r → Quiver.Star x

The first arrow of a surviving relation-support path.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportInitialArrow_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)) : Function.Injective (P.relationSurvivingSupportInitialArrow r hr)

Surviving paths in one displayed relation have distinct first arrows.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_natCard_le_two {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)) : Nat.card (P.RelationSurvivingSupport r) ≤ 2

At most two paths occurring in one displayed relation can survive in the original special-biserial quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.RelationSurvivingSupport.exists_ne {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) : ∃ (q : P.RelationSurvivingSupport r), q ≠ p

A surviving path in a displayed relation is paired with a distinct surviving path in that same relation.

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.FinalDecomposition {Q : Type u} [Quiver Q] {x z : Q} (p : Quiver.Path x z) : Type u

A nonempty path decomposed into an initial segment and final arrow.

• middle : Q
• head : Quiver.Path x self.middle
• arrow : self.middle ⟶ z
• path_eq : p = self.head.comp self.arrow.toPath
• length_eq : p.length = self.head.length + 1

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFinalDecomposition {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) : FinalDecomposition ↑p

A chosen final-arrow decomposition for a surviving relation-support path.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFinalArrow {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.RelationSurvivingSupport r → Quiver.Costar z

The final arrow of a surviving relation-support path.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFinalArrow_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)) : Function.Injective (P.relationSurvivingSupportFinalArrow r hr)

Surviving paths in one displayed relation have distinct final arrows.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_finite {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)) : Finite (P.RelationSurvivingSupport r)

The surviving support of a displayed relation is finite.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_natCard_eq_two {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) : Nat.card (P.RelationSurvivingSupport r) = 2

A displayed relation with one surviving path has exactly two surviving path terms.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportInitialArrow_bijective {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) : Function.Bijective (P.relationSurvivingSupportInitialArrow r hr)

Once a displayed relation has a surviving term, its two terms exhaust the arrows leaving their common initial vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFinalArrow_bijective {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) : Function.Bijective (P.relationSurvivingSupportFinalArrow r hr)

Once a displayed relation has a surviving term, its two terms exhaust the arrows entering their common terminal vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.RelationSurvivingSupport.existsUnique_ne {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) : ∃! q : P.RelationSurvivingSupport r, q ≠ p

Every surviving path has a unique distinct partner in its displayed relation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relation_pathMap_sum_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 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)) : ∑ q ∈ ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r).support, ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) q • pathMap P.relations q = 0

The displayed relation maps to the corresponding coefficient sum of path classes, which vanishes in the original quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_pair_smul_add_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 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 q : P.RelationSurvivingSupport r) (hqp : q ≠ p) : ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) ↑p • pathMap P.relations ↑p + ((LinearPathCategory.homPathLinearEquiv (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) r) ↑q • pathMap P.relations ↑q = 0

The two surviving path classes in a displayed relation satisfy its literal two-term linear relation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupport_pathMap_eq_smul {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 q : P.RelationSurvivingSupport r) (hqp : q ≠ p) : ∃ (c : k), c ≠ 0 ∧ pathMap P.relations ↑p = c • pathMap P.relations ↑q

The two surviving path classes in one displayed relation are nonzero scalar multiples of one another.