Path bases for arrow-generated ideals

For a monomial special-biserial presentation, composition with one displayed arrow has a basis indexed by the surviving continuations of that arrow. The continuation basis has at most one vector in every path length by StringPathCombinatorics. These are the pointwise path bases underlying the uniserial modules aA in the string-algebra argument of the frozen manuscript.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.RightContinuationAt {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Type u

Surviving continuations from the endpoint of a to a fixed vertex z. They index the z-coordinate of the right ideal generated by a.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.rightArrowCompositionLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : (obj P.relations z ⟶ obj P.relations y) →ₗ[k] obj P.relations z ⟶ obj P.relations x

Postcomposition by the image of a, in the reversed categorical orientation of the bound-quiver category.

def MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAtToSurviving {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.RightContinuationAt a z → SurvivingPath P.relations x z

A continuation indexes its concatenated surviving path.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAtToSurviving_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.rightContinuationAtToSurviving a z)

Concatenation with a fixed initial arrow is injective.

def MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAtToPath {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.RightContinuationAt a z → P.RightContinuationPath a

A fixed-endpoint continuation is a continuation with varying endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAtToPath_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.rightContinuationAtToPath a z)

Forgetting a fixed endpoint is injective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAt_finite {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Finite (P.RightContinuationAt a z)

Fixed-endpoint continuations form a finite type.

def MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAtLengthEmbedding {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.RightContinuationAt a z ↪ ℕ

Path length embeds the fixed-endpoint continuation basis into the natural numbers.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAt_pathMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) (q : P.RightContinuationAt a z) : pathMap P.relations ↑(P.rightContinuationAtToSurviving a z q) = (P.rightArrowCompositionLinearMap a z) (pathMap P.relations ↑q)

The concatenated path map is the corresponding arrow-composition image.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightContinuationAt_linearIndependent {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : LinearIndependent k fun (q : P.RightContinuationAt a z) => (P.rightArrowCompositionLinearMap a z) (pathMap P.relations ↑q)

Concatenated surviving continuations of an arrow are linearly independent.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.span_rightContinuationAt_eq_range {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Submodule.span k (Set.range fun (q : P.RightContinuationAt a z) => (P.rightArrowCompositionLinearMap a z) (pathMap P.relations ↑q)) = (P.rightArrowCompositionLinearMap a z).range

The surviving continuations span the image of composition with a.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.rightArrowCoordinateBasis {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.Basis (P.RightContinuationAt a z) k ↥(P.rightArrowCompositionLinearMap a z).range

The pointwise arrow-generated subspace has its literal continuation-path basis.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_rightArrowCompositionRange_eq_natCard {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.finrank k ↥(P.rightArrowCompositionLinearMap a z).range = Nat.card (P.RightContinuationAt a z)

The dimension of one coordinate of the arrow-generated ideal is the number of surviving paths ending there which begin with the chosen arrow.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.LeftContinuationAt {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Type u

Surviving continuations from a fixed vertex z to the source of a. They index the z-coordinate of the categorical right ideal represented by the displayed arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCompositionLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : (obj P.relations x ⟶ obj P.relations z) →ₗ[k] obj P.relations y ⟶ obj P.relations z

Precomposition by the image of a, in the reversed categorical orientation of the bound-quiver category.

def MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAtToSurviving {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.LeftContinuationAt a z → SurvivingPath P.relations z y

A left continuation indexes its concatenated surviving path.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAtToSurviving_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.leftContinuationAtToSurviving a z)

Concatenation with a fixed final arrow is injective.

def MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAtToPath {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.LeftContinuationAt a z → P.LeftContinuationPath a

A fixed-startpoint left continuation is a continuation with varying startpoint.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAtToPath_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.leftContinuationAtToPath a z)

Forgetting a fixed startpoint is injective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAt_finite {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Finite (P.LeftContinuationAt a z)

Fixed-startpoint left continuations form a finite type.

def MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAtLengthEmbedding {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : P.LeftContinuationAt a z ↪ ℕ

Path length embeds the fixed-startpoint left continuation basis into the natural numbers.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAt_pathMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) (p : P.LeftContinuationAt a z) : pathMap P.relations ↑(P.leftContinuationAtToSurviving a z p) = (P.leftArrowCompositionLinearMap a z) (pathMap P.relations ↑p)

The concatenated path map is the corresponding left-composition image.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationAt_linearIndependent {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : LinearIndependent k fun (p : P.LeftContinuationAt a z) => (P.leftArrowCompositionLinearMap a z) (pathMap P.relations ↑p)

Concatenated surviving left continuations of an arrow are linearly independent.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.span_leftContinuationAt_eq_range {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Submodule.span k (Set.range fun (p : P.LeftContinuationAt a z) => (P.leftArrowCompositionLinearMap a z) (pathMap P.relations ↑p)) = (P.leftArrowCompositionLinearMap a z).range

The surviving left continuations span the image of composition with a.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCoordinateBasis {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.Basis (P.LeftContinuationAt a z) k ↥(P.leftArrowCompositionLinearMap a z).range

The pointwise categorical arrow-generated subspace has its literal left continuation-path basis.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCoordinateBasis_apply {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) (p : P.LeftContinuationAt a z) : (P.leftArrowCoordinateBasis a z) p = ⟨(P.leftArrowCompositionLinearMap a z) (pathMap P.relations ↑p), ⋯⟩

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_leftArrowCompositionRange_eq_natCard {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.finrank k ↥(P.leftArrowCompositionLinearMap a z).range = Nat.card (P.LeftContinuationAt a z)

The dimension of one coordinate of the categorical right arrow ideal is the number of surviving paths starting there which end with the chosen arrow.