theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.finiteDualCorepresentablesOfAdmissible {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : Category R) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule X)

Admissibility over a finite quiver also makes every coefficient-dual corepresentable finite-dimensional with finite support.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFunctional {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) : Module.Dual k (obj P.relations z ⟶ obj P.relations x)

A normalized functional detecting one nonzero surviving relation path class.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportFunctional_pathMap {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.relationSurvivingSupportFunctional r hr p) (pathMap P.relations ↑p) = 1

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSourceRepresentable {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) : CoveringHom.FiniteDimensionalModuleCategory k

The finite covariant representable whose path basis consists of paths ending at z.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationTargetDualCorepresentable {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 : Q) : CoveringHom.FiniteDimensionalModuleCategory k

The finite dual corepresentable whose dual path coordinates consist of paths beginning at x.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportNakayamaHom {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.relationSourceRepresentable z ⟶ P.relationTargetDualCorepresentable x

A surviving relation path class induces the composition-pairing map from the representable at its terminal vertex to the dual corepresentable at its initial vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportNakayamaHom_app_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) (f : obj P.relations z ⟶ Y) (g : Y ⟶ obj P.relations x) : (have this := (CategoryTheory.ConcreteCategory.hom ((P.relationSurvivingSupportNakayamaHom r hr p).hom.hom.app Y)) f; this) g = (P.relationSurvivingSupportFunctional r hr p) (CategoryTheory.CategoryStruct.comp f g)

The induced module map is literally composition followed by the chosen path-detecting functional.

def 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) : Prop

The exact remaining combinatorial property needed to identify the two endpoint modules attached to a paired maximal relation path.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSurvivingSupportNakayamaHom_isIso {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) (hperfect : P.HasPerfectRelationPairing r hr p) : CategoryTheory.IsIso (P.relationSurvivingSupportNakayamaHom r hr p)

A perfect composition pairing makes the relation-induced module map an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSourceRepresentable_injective_of_perfect {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) (hperfect : P.HasPerfectRelationPairing r hr p) : CategoryTheory.Injective (P.relationSourceRepresentable z)

The representable ending at a paired maximal relation path is injective once its composition pairing is perfect.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.survivingPath_ending_relationSupport_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 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) : ∃ (t : P.RelationSurvivingSupport r) (g : Quiver.Path x y), ↑t = g.comp ↑s

Every surviving path ending at the terminal vertex of a paired maximal relation path is a suffix of one of the two relation-support paths.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.survivingPath_starting_relationSupport_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 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) : ∃ (t : P.RelationSurvivingSupport r) (h : Quiver.Path y z), ↑t = (↑s).comp h

Every surviving path beginning at the initial vertex of a paired maximal relation path is a prefix of one of the two relation-support paths.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.survivingPath_ending_hullKernel_relationSupport {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) (hsHull : pathMap (pathSupportHull P.relations) ↑s = 0) : ∃ (t : P.RelationSurvivingSupport r) (g : Quiver.Path x y), ↑t = g.comp ↑s ∧ g.length = 0

If a surviving path into the paired terminal vertex is killed by the path-support-hull quotient, then it is itself one of the two maximal relation paths: its complementary prefix has length zero.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.survivingPath_starting_hullKernel_relationSupport {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) (hsHull : pathMap (pathSupportHull P.relations) ↑s = 0) : ∃ (t : P.RelationSurvivingSupport r) (h : Quiver.Path y z), ↑t = (↑s).comp h ∧ h.length = 0

If a surviving path out of the paired initial vertex is killed by the path-support-hull quotient, then it is itself one of the two maximal relation paths: its complementary suffix has length zero.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_endpoint_eq_span_relationSupport {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) : (relativeRelationHomIdeal ⋯).homSubmodule (obj P.relations z) (obj P.relations x) = Submodule.span k (Set.range fun (t : P.RelationSurvivingSupport r) => pathMap P.relations ↑t)

At the two endpoints of a paired relation, the support-hull kernel is spanned by precisely the surviving paths displayed in that relation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_endpoint_eq_span_singleton {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) : (relativeRelationHomIdeal ⋯).homSubmodule (obj P.relations z) (obj P.relations x) = k ∙ pathMap P.relations ↑p

The endpoint kernel coordinate is the line generated by either one of the two surviving relation-path classes.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_terminalCoordinate_eq_bot_of_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) {y : Q} (hyx : y ≠ x) : (relativeRelationHomIdeal ⋯).homSubmodule (obj P.relations z) (obj P.relations y) = ⊥

Away from the initial endpoint, the terminal row of the support-hull kernel vanishes.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativePathSupportHull_initialCoordinate_eq_bot_of_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) {y : Q} (hyz : y ≠ z) : (relativeRelationHomIdeal ⋯).homSubmodule (obj P.relations y) (obj P.relations x) = ⊥

Away from the terminal endpoint, the initial column of the support-hull kernel vanishes.