Iterated endpoint extensions of string modules

An extension arm records a finite sequence of same-sign letters appended at the right endpoint of a string. Negative arms compose the canonical one-letter inclusions; positive arms compose the canonical one-letter projections in the reverse direction.

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Word R → Type u

A finite sequence of negative letters appended to C.

• base {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} : C.NegativeExtension C
• step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) {z : Q} (a : z ⟶ D.target) (h : IsString R (Quiver.Path.comp D.path (Quiver.Hom.toPath (negativeArrow a)))) : C.NegativeExtension (append R D (negativeArrow a) h)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.source_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : D.source = C.source

A negative arm does not change the source vertex.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.ordinaryPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.NegativeExtension D → Quiver.Path D.target C.target

The ordinary displayed-quiver path traversed by a negative arm, from its new endpoint back to the original endpoint.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.NegativeExtension D → ℕ

Number of letters in a negative extension arm.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.ordinaryPath_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : arm.ordinaryPath.length = arm.steps

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.exists_reverse_suffix {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : ∃ (r : SignedPath C.target D.source), Quiver.Path.reverse D.path = Quiver.Path.comp (positivePath arm.ordinaryPath) r

Reversing the final word exposes the negative arm as a positive ordinary prefix.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.positivePath_ordinaryPath_contiguous_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : IsContiguousSubpath (positivePath arm.ordinaryPath) (Quiver.Path.reverse D.path)

The ordinary path of a negative arm occurs positively in the reversed final word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.pathMap_ordinaryPath_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : pathMap R arm.ordinaryPath ≠ 0

The ordinary path underlying a negative arm survives the relation quotient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.steps_lt_of_long_paths_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) {N : ℕ} (hlong : ∀ {x y : Q} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)) : arm.steps < N

Any uniform admissibility bound for killed ordinary paths strictly bounds the number of steps in a negative arm.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.result_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : length R D = length R C + arm.steps

The endpoint word is longer by exactly the number of arm steps.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.NegativeExtension D) (second : D.NegativeExtension E) : C.NegativeExtension E

Concatenate two negative extension arms.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.steps_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.NegativeExtension D) (second : D.NegativeExtension E) : (first.trans second).steps = first.steps + second.steps

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.exists_prefix_of_steps_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) {n : ℕ} (hn : n ≤ arm.steps) : ∃ (E : Word R) (initial : C.NegativeExtension E), initial.steps = n ∧ ∃ (suffix : E.NegativeExtension D), initial.trans suffix = arm

Every initial number of steps of a negative arm is represented by a prefix arm, followed by a residual negative arm.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.moduleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) (hmono : IsMonomial R) : C.rightModule hmono ⟶ D.rightModule hmono

The composite right-module inclusion along a negative extension arm.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.moduleMap_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) (hmono : IsMonomial R) : CategoryTheory.Mono (arm.moduleMap hmono)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.moduleMap_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.NegativeExtension D) (second : D.NegativeExtension E) (hmono : IsMonomial R) : (first.trans second).moduleMap hmono = CategoryTheory.CategoryStruct.comp (first.moduleMap hmono) (second.moduleMap hmono)

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Word R → Type u

A finite sequence of positive letters appended to C.

• base {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} : C.PositiveExtension C
• step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) {z : Q} (a : D.target ⟶ z) (h : IsString R (Quiver.Path.comp D.path (Quiver.Hom.toPath (positiveArrow a)))) : C.PositiveExtension (append R D (positiveArrow a) h)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.source_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : D.source = C.source

A positive arm does not change the source vertex.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.ordinaryPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.PositiveExtension D → Quiver.Path C.target D.target

The ordinary displayed-quiver path traversed by a positive arm, from the original endpoint to its new endpoint.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.PositiveExtension D → ℕ

Number of letters in a positive extension arm.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.ordinaryPath_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : arm.ordinaryPath.length = arm.steps

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.exists_path_prefix {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : ∃ (l : SignedPath D.source C.target), D.path = Quiver.Path.comp l (positivePath arm.ordinaryPath)

The positive ordinary path of an arm is a suffix of the final word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.positivePath_ordinaryPath_contiguous {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : IsContiguousSubpath (positivePath arm.ordinaryPath) D.path

The ordinary path of a positive arm occurs positively in the final word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.pathMap_ordinaryPath_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : pathMap R arm.ordinaryPath ≠ 0

The ordinary path underlying a positive arm survives the relation quotient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.steps_lt_of_long_paths_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) {N : ℕ} (hlong : ∀ {x y : Q} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)) : arm.steps < N

Any uniform admissibility bound for killed ordinary paths strictly bounds the number of steps in a positive arm.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.result_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : length R D = length R C + arm.steps

The endpoint word is longer by exactly the number of arm steps.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.PositiveExtension D) (second : D.PositiveExtension E) : C.PositiveExtension E

Concatenate two positive extension arms.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.steps_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.PositiveExtension D) (second : D.PositiveExtension E) : (first.trans second).steps = first.steps + second.steps

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.exists_prefix_of_steps_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) {n : ℕ} (hn : n ≤ arm.steps) : ∃ (E : Word R) (initial : C.PositiveExtension E), initial.steps = n ∧ ∃ (suffix : E.PositiveExtension D), initial.trans suffix = arm

Every initial number of steps of a positive arm is represented by a prefix arm, followed by a residual positive arm.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.moduleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) (hmono : IsMonomial R) : D.rightModule hmono ⟶ C.rightModule hmono

The composite right-module projection along a positive extension arm.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.moduleMap_epi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) (hmono : IsMonomial R) : CategoryTheory.Epi (arm.moduleMap hmono)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.moduleMap_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.PositiveExtension D) (second : D.PositiveExtension E) (hmono : IsMonomial R) : (first.trans second).moduleMap hmono = CategoryTheory.CategoryStruct.comp (second.moduleMap hmono) (first.moduleMap hmono)