Deterministic path continuations in string presentations

The special-biserial continuation conditions make every nonzero path beyond a fixed initial arrow deterministic. This file packages that statement with path length retained, which is the combinatorial input for the uniserial arrow ideals and string modules used in the frozen manuscript.

@[reducible, inline]

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

The arrows which can follow a without making the two-arrow path zero.

@[reducible, inline]

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

The arrows which can precede a without making the two-arrow path zero.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationArrow_subsingleton {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) : Subsingleton (P.RightContinuationArrow a)

There is at most one nonzero right continuation of an arrow.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationArrow_subsingleton {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) : Subsingleton (P.LeftContinuationArrow a)

There is at most one nonzero left continuation of an arrow.

@[reducible, inline]

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

All nonzero path continuations after a, with endpoint retained.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationPathToSurviving {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) : P.RightContinuationPath a → (z : Q) × SurvivingPath P.relations x z

Concatenating the fixed initial arrow embeds its nonzero continuations into the surviving paths of the quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationPathToSurviving_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 y : Q} (a : x ⟶ y) : Function.Injective (P.rightContinuationPathToSurviving a)

Distinct continuations remain distinct after adjoining their common initial arrow.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationPath_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 y : Q} (a : x ⟶ y) : Finite (P.RightContinuationPath a)

Admissibility makes the complete set of nonzero continuations of one arrow finite.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.RightContinuationPathAtLength {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) (n : ℕ) : Type u

A nonzero path of prescribed additional length after the arrow a. The endpoint is retained in the sigma type.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationPathAtLength_subsingleton {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) (n : ℕ) {x y : Q} (a : x ⟶ y) : Subsingleton (P.RightContinuationPathAtLength a n)

Beyond a fixed initial arrow, a nonzero path is uniquely determined by its additional length.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.natCard_rightContinuationPathAtLength_le_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 : Q} (a : x ⟶ y) (n : ℕ) : Nat.card (P.RightContinuationPathAtLength a n) ≤ 1

The set of nonzero right continuations of any fixed length has cardinality at most one.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationLengthEmbedding {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) : P.RightContinuationPath a ↪ ℕ

Length embeds the complete finite set of nonzero right continuations into the natural numbers. Thus those continuations form one chain, with no branching at any radical layer.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationPath_factor_of_length_le {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) (p q : P.RightContinuationPath a) (h : (↑p).snd.length ≤ (↑q).snd.length) : ∃ (r : Quiver.Path (↑p).fst (↑q).fst), (↑q).snd = (↑p).snd.comp r

A longer surviving right continuation factors through every shorter one. The factor is the final segment between their endpoints.

@[reducible, inline]

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

Surviving right continuations of a with one fixed endpoint.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationAtToPath {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.RightContinuationAt a z → P.RightContinuationPath a

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

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.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 : SpecialBiserialPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.rightContinuationAtToPath a z)

Forgetting that the endpoint was fixed is injective.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.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 : SpecialBiserialPresentation 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.SpecialBiserialPresentation.rightContinuationAtLengthEmbedding {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.RightContinuationAt a z ↪ ℕ

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

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationAt_factor_of_length_le {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) (h : (↑p).length ≤ (↑q).length) : ∃ (r : Quiver.Path z z), ↑q = (↑p).comp r

At a fixed endpoint, every longer continuation is obtained from every shorter one by adjoining a loop at that endpoint.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.rightContinuationAt_factor_of_length_lt {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) (h : (↑p).length < (↑q).length) : ∃ (r : Quiver.Path z z), ↑q = (↑p).comp r ∧ r.length ≠ 0

A strict increase in continuation length gives a positive-length loop factor at the common endpoint.

@[reducible, inline]

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

All nonzero path continuations before a, with starting vertex retained.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPathToSurviving {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) : P.LeftContinuationPath a → (z : Q) × SurvivingPath P.relations z y

Concatenating the fixed final arrow embeds its nonzero left continuations into the surviving paths of the quotient.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPathToSurviving_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 y : Q} (a : x ⟶ y) : Function.Injective (P.leftContinuationPathToSurviving a)

Distinct left continuations remain distinct after adjoining their common final arrow.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPath_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 y : Q} (a : x ⟶ y) : Finite (P.LeftContinuationPath a)

Admissibility makes the complete set of nonzero left continuations of one arrow finite.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.LeftContinuationPathAtLength {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) (n : ℕ) : Type u

A nonzero path of prescribed additional length before the arrow a. The starting vertex is retained in the sigma type.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPathAtLength_subsingleton {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) (n : ℕ) {x y : Q} (a : x ⟶ y) : Subsingleton (P.LeftContinuationPathAtLength a n)

Before a fixed final arrow, a nonzero path is uniquely determined by its additional length.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.natCard_leftContinuationPathAtLength_le_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 : Q} (a : x ⟶ y) (n : ℕ) : Nat.card (P.LeftContinuationPathAtLength a n) ≤ 1

The set of nonzero left continuations of any fixed length has cardinality at most one.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationLengthEmbedding {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) : P.LeftContinuationPath a ↪ ℕ

Length embeds the complete finite set of nonzero left continuations into the natural numbers.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPath_factor_of_length_le {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) (p q : P.LeftContinuationPath a) (h : (↑p).snd.length ≤ (↑q).snd.length) : ∃ (r : Quiver.Path (↑q).fst (↑p).fst), (↑q).snd = r.comp (↑p).snd

A longer surviving left continuation factors through every shorter one. The factor is the initial segment between their starting vertices.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationPath_factor_of_length_lt {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) (p q : P.LeftContinuationPath a) (h : (↑p).snd.length < (↑q).snd.length) : ∃ (r : Quiver.Path (↑q).fst (↑p).fst), (↑q).snd = r.comp (↑p).snd ∧ r.length ≠ 0

Under a strict length inequality, the initial factor between two left continuations has positive length.

@[reducible, inline]

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

Surviving left continuations of a with one fixed starting vertex.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationAtToPath {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.LeftContinuationAt a z → P.LeftContinuationPath a

A fixed-start continuation is in particular a continuation with varying starting vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.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 : SpecialBiserialPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Function.Injective (P.leftContinuationAtToPath a z)

Forgetting that the starting vertex was fixed is injective.

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

Fixed-start continuations form a finite type.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationAtLengthEmbedding {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.LeftContinuationAt a z ↪ ℕ

Path length embeds the fixed-start continuation chain into the natural numbers.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationAt_factor_of_length_le {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) (h : (↑p).length ≤ (↑q).length) : ∃ (r : Quiver.Path z z), ↑q = r.comp ↑p

At a fixed starting vertex, every longer left continuation is obtained from every shorter one by adjoining a loop at that vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.leftContinuationAt_factor_of_length_lt {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) (h : (↑p).length < (↑q).length) : ∃ (r : Quiver.Path z z), ↑q = r.comp ↑p ∧ r.length ≠ 0

A strict increase in left-continuation length gives a positive-length loop factor at the common starting vertex.