The path action on a string-arrow right ideal

Longer surviving continuations factor through shorter ones. This file realizes the intervening path as a matrix coordinate in the finite category algebra and computes its action on the global continuation basis.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.pathRepresentableMap {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) {z x : Q} (p : Quiver.Path z x) : P.quotientRepresentable (obj P.relations z) ⟶ P.quotientRepresentable (obj P.relations x)

The representable transformation induced by an arbitrary displayed path.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathRepresentableMap_app_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) {z x : Q} (p : Quiver.Path z x) (w : Q) (f : obj P.relations z ⟶ obj P.relations w) : (ModuleCat.Hom.hom ((P.pathRepresentableMap p).hom.hom.app (obj P.relations w))) f = CategoryTheory.CategoryStruct.comp (pathMap P.relations p) f

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathRepresentableMap_comp {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) {w z x : Q} (r : Quiver.Path w z) (p : Quiver.Path z x) : CategoryTheory.CategoryStruct.comp (P.pathRepresentableMap r) (P.pathRepresentableMap p) = P.pathRepresentableMap (r.comp p)

Concatenation of displayed paths becomes composition of the induced representable transformations.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathRepresentableMap_comp_arrowRepresentableMap_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 : StringPresentation k A Q) {w x y : Q} (a : x ⟶ y) (p : Quiver.Path w x) (hzero : CategoryTheory.CategoryStruct.comp (arrowMap P.relations a) (pathMap P.relations p) = 0) : CategoryTheory.CategoryStruct.comp (P.pathRepresentableMap p) (P.arrowRepresentableMap a) = 0

A killed path after the displayed arrow induces the zero composite of representable transformations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate {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) {z x : Q} (p : Quiver.Path z x) : P.quotientCategoryAlgebra

The matrix coordinate of an arbitrary displayed path in the finite category algebra.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowModuleBasis {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) : Module.Basis (P.LeftContinuationPath a) k ↥(P.representedArrowLinearMap a).range

The algebra-linear represented range has the same continuation basis as its coefficient-field-linear realization.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedContinuationElement {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) (p : P.LeftContinuationPath a) : ↥(P.representedArrowLinearMap a).range

The explicit represented-range element belonging to one surviving left continuation.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedContinuationElement_coordinate_self {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) (p : P.LeftContinuationPath a) : (P.representedArrowRangeCoordinateLinearEquiv a) ((P.representedArrowRangeKLinearEquiv a) (P.representedContinuationElement a p)) (obj P.relations (↑p).fst) = (P.leftArrowCoordinateBasis a (↑p).fst) ⟨(↑p).snd, ⋯⟩

The explicit continuation element has its path vector at its starting vertex.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedContinuationElement_coordinate_ne {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) (p : P.LeftContinuationPath a) (z : Q) (hz : z ≠ (↑p).fst) : (P.representedArrowRangeCoordinateLinearEquiv a) ((P.representedArrowRangeKLinearEquiv a) (P.representedContinuationElement a p)) (obj P.relations z) = 0

The explicit continuation element vanishes in every other starting vertex coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowModuleBasis_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) (p : P.LeftContinuationPath a) : (P.representedArrowModuleBasis a) p = P.representedContinuationElement a p

The transported global basis vector is the explicit matrix-supported continuation element.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRange_smul_val {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) (c : P.quotientCategoryAlgebraᵐᵒᵖ) (g : ↥(P.representedArrowLinearMap a).range) : ↑(c • g) = CategoryTheory.CategoryStruct.comp (MulOpposite.unop c) ↑g

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedContinuationElement {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) (p q : P.LeftContinuationPath a) (r : Quiver.Path (↑q).fst (↑p).fst) (hr : (↑q).snd = r.comp (↑p).snd) : MulOpposite.op (P.pathAlgebraCoordinate r) • P.representedContinuationElement a p = P.representedContinuationElement a q

The matrix coordinate of the factor between two continuations sends the shorter explicit continuation element to the longer one.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedArrowModuleBasis {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) (p q : P.LeftContinuationPath a) (r : Quiver.Path (↑q).fst (↑p).fst) (hr : (↑q).snd = r.comp (↑p).snd) : MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = (P.representedArrowModuleBasis a) q

The same path-coordinate action, stated on the transported global basis.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowModuleBasis_smul_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 : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (p q : P.LeftContinuationPath a) (h : (↑p).snd.length ≤ (↑q).snd.length) : ∃ (c : P.quotientCategoryAlgebraᵐᵒᵖ), c • (P.representedArrowModuleBasis a) p = (P.representedArrowModuleBasis a) q

Every longer continuation-basis vector is an algebra multiple of every shorter one.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedArrowModuleBasis_eq_zero_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 : StringPresentation k A Q) {x y w z : Q} (a : x ⟶ y) (r : Quiver.Path w z) (p : P.LeftContinuationPath a) (hz : z ≠ (↑p).fst) : MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = 0

A path coordinate whose target does not match the starting vertex of a continuation kills its basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedArrowModuleBasis_eq_zero_of_comp {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 w : Q} (a : x ⟶ y) (p : P.LeftContinuationPath a) (r : Quiver.Path w (↑p).fst) (hzero : CategoryTheory.CategoryStruct.comp (arrowMap P.relations a) (pathMap P.relations (r.comp (↑p).snd)) = 0) : MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = 0

When the concatenated path is killed after the arrow, the matching path coordinate kills the continuation basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedArrowModuleBasis_eq_zero_or {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 w : Q} (a : x ⟶ y) (p : P.LeftContinuationPath a) (r : Quiver.Path w (↑p).fst) : MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = 0 ∨ ∃ (q : P.LeftContinuationPath a), (↑q).snd.length = r.length + (↑p).snd.length ∧ MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = (P.representedArrowModuleBasis a) q

A path coordinate acts on any continuation basis vector either by zero or by the basis vector of the surviving concatenation.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_representedArrowModuleBasis_eq_zero_or_any {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 w z : Q} (a : x ⟶ y) (p : P.LeftContinuationPath a) (r : Quiver.Path w z) : MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = 0 ∨ ∃ (q : P.LeftContinuationPath a), (↑q).snd.length = r.length + (↑p).snd.length ∧ MulOpposite.op (P.pathAlgebraCoordinate r) • (P.representedArrowModuleBasis a) p = (P.representedArrowModuleBasis a) q

An arbitrary path coordinate acts on a continuation basis vector either by zero or by a basis vector whose length increases by the path length.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLengthTail {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) (m : ℕ) : Submodule k ↥(P.representedArrowLinearMap a).range

The subspace spanned by continuation-basis vectors of length at least m.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowModuleBasis_mem_lengthTail {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) (m : ℕ) (p : P.LeftContinuationPath a) (hp : m ≤ (↑p).snd.length) : (P.representedArrowModuleBasis a) p ∈ P.representedArrowLengthTail a m

A continuation-basis vector belongs to every length tail below its length.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLengthTail_antitone {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) {m n : ℕ} (hmn : m ≤ n) : P.representedArrowLengthTail a n ≤ P.representedArrowLengthTail a m

Requiring a larger minimum length gives a smaller tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLengthTail_eq_bot_of_forall_lt {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) (n : ℕ) (hn : ∀ (p : P.LeftContinuationPath a), (↑p).snd.length < n) : P.representedArrowLengthTail a n = ⊥

A length tail beyond every surviving continuation is zero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_representedArrowLengthTail_eq_bot {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) : ∃ (n : ℕ), P.representedArrowLengthTail a n = ⊥

Admissibility makes one sufficiently deep continuation-length tail zero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pathAlgebraCoordinate_smul_mem_lengthTail {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 w z : Q} (a : x ⟶ y) (r : Quiver.Path w z) (m : ℕ) (g : ↥(P.representedArrowLinearMap a).range) (hg : g ∈ P.representedArrowLengthTail a m) : MulOpposite.op (P.pathAlgebraCoordinate r) • g ∈ P.representedArrowLengthTail a (m + r.length)

Acting by a path coordinate raises the length tail by the length of the path.

def MagnitudeConjecture.BoundQuiver.StringPresentation.RaisesRepresentedArrowLengthTail {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) (c : P.quotientCategoryAlgebraᵐᵒᵖ) : Prop

A category-algebra scalar is positive on an arrow module when it raises every continuation-length tail by one.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.raisesRepresentedArrowLengthTail_pathAlgebraCoordinate {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 w z : Q} (a : x ⟶ y) (r : Quiver.Path w z) (hr : r.length ≠ 0) : P.RaisesRepresentedArrowLengthTail a (MulOpposite.op (P.pathAlgebraCoordinate r))

A positive-length path coordinate raises every length tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.raisesRepresentedArrowLengthTail_zero {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) : P.RaisesRepresentedArrowLengthTail a 0

Zero raises every length tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.RaisesRepresentedArrowLengthTail.add {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) {c d : P.quotientCategoryAlgebraᵐᵒᵖ} (hc : P.RaisesRepresentedArrowLengthTail a c) (hd : P.RaisesRepresentedArrowLengthTail a d) : P.RaisesRepresentedArrowLengthTail a (c + d)

Sums of tail-raising scalars still raise tails.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.raisesRepresentedArrowLengthTail_finset_sum {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) {I : Type u_1} (s : Finset I) (f : I → P.quotientCategoryAlgebraᵐᵒᵖ) (hf : ∀ i ∈ s, P.RaisesRepresentedArrowLengthTail a (f i)) : P.RaisesRepresentedArrowLengthTail a (∑ i ∈ s, f i)

A finite sum of tail-raising scalars raises tails.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.RaisesRepresentedArrowLengthTail.algebraMap_mul {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) {d : P.quotientCategoryAlgebraᵐᵒᵖ} (hd : P.RaisesRepresentedArrowLengthTail a d) (c : k) : P.RaisesRepresentedArrowLengthTail a ((algebraMap k P.quotientCategoryAlgebraᵐᵒᵖ) c * d)

Multiplying a tail-raising scalar by a field scalar preserves the tail-raising property.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_raisesRepresentedArrowLengthTail_smul_basis_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 : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (p q : P.LeftContinuationPath a) (hpq : (↑p).snd.length < (↑q).snd.length) : ∃ (c : P.quotientCategoryAlgebraᵐᵒᵖ), P.RaisesRepresentedArrowLengthTail a c ∧ c • (P.representedArrowModuleBasis a) p = (P.representedArrowModuleBasis a) q

A strictly longer continuation is obtained from a shorter one by a tail-raising scalar.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.RaisesRepresentedArrowLengthTail.pow_smul_mem {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) {c : P.quotientCategoryAlgebraᵐᵒᵖ} (hc : P.RaisesRepresentedArrowLengthTail a c) (n m : ℕ) (g : ↥(P.representedArrowLinearMap a).range) (hg : g ∈ P.representedArrowLengthTail a m) : c ^ n • g ∈ P.representedArrowLengthTail a (m + n)

The nth power of a tail-raising scalar raises length by n.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.RaisesRepresentedArrowLengthTail.exists_pow_smul_basis_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 : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) {c : P.quotientCategoryAlgebraᵐᵒᵖ} (hc : P.RaisesRepresentedArrowLengthTail a c) (p : P.LeftContinuationPath a) : ∃ (n : ℕ), c ^ n • (P.representedArrowModuleBasis a) p = 0

A tail-raising scalar acts locally nilpotently on each continuation-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_raisesRepresentedArrowLengthTail_smul_basis_eq_sub {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) (g : ↥(P.representedArrowLinearMap a).range) (p : P.LeftContinuationPath a) (hp : ((P.representedArrowModuleBasis a).repr g) p ≠ 0) (hmin : ∀ (q : P.LeftContinuationPath a), ((P.representedArrowModuleBasis a).repr g) q ≠ 0 → (↑p).snd.length ≤ (↑q).snd.length) : ∃ (n : P.quotientCategoryAlgebraᵐᵒᵖ), P.RaisesRepresentedArrowLengthTail a n ∧ n • (P.representedArrowModuleBasis a) p = g - ((P.representedArrowModuleBasis a).repr g) p • (P.representedArrowModuleBasis a) p

After selecting a nonzero shortest coordinate of a vector, all remaining coordinates are produced from that basis vector by one tail-raising scalar.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_mutually_smul_basis_of_minimal_repr {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) (g : ↥(P.representedArrowLinearMap a).range) (p : P.LeftContinuationPath a) (hp : ((P.representedArrowModuleBasis a).repr g) p ≠ 0) (hmin : ∀ (q : P.LeftContinuationPath a), ((P.representedArrowModuleBasis a).repr g) q ≠ 0 → (↑p).snd.length ≤ (↑q).snd.length) : ∃ (c : P.quotientCategoryAlgebraᵐᵒᵖ) (d : P.quotientCategoryAlgebraᵐᵒᵖ), c • (P.representedArrowModuleBasis a) p = g ∧ d • g = (P.representedArrowModuleBasis a) p

A nonzero shortest basis coordinate and its vector generate one another under the category-algebra action.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_mutually_smul_basis_of_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 : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (g : ↥(P.representedArrowLinearMap a).range) (hg : g ≠ 0) : ∃ (p : P.LeftContinuationPath a) (c : P.quotientCategoryAlgebraᵐᵒᵖ) (d : P.quotientCategoryAlgebraᵐᵒᵖ), c • (P.representedArrowModuleBasis a) p = g ∧ d • g = (P.representedArrowModuleBasis a) p

Every nonzero represented arrow-module vector is mutually cyclic with its shortest continuation-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearRange_isUniserial {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) : IsUniserialModule P.quotientCategoryAlgebraᵐᵒᵖ ↥(P.representedArrowLinearMap a).range

The represented range of a string arrow is a uniserial module over the opposite finite category algebra.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRightIdeal_isUniserial {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) : IsUniserialModule P.quotientCategoryAlgebraᵐᵒᵖ ↥(RightModule.rightIdeal (P.arrowAlgebraCoordinate a))

The literal principal right ideal generated by a string arrow is uniserial.