The canonical kernel word of a displayed hook arrow

The negative tail after a positive hook boundary is independent of the word before that boundary. More precisely, its positive reversal is determined by the displayed central arrow. The proof splits a nonempty tail at the arrow adjacent to the center: the degree-two condition determines that arrow, and special-biserial continuation uniqueness determines the remaining path at each fixed length. Replaying a hook onto the trivial source word shows that maximal tails have the same length.

@[simp]

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

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

The first arrow adjacent to the base of a nonempty negative extension, together with the path before it.

• vertex : Q
• arrow : self.vertex ⟶ C.target
• initialPath : Quiver.Path D.target self.vertex
• path_eq : arm.ordinaryPath = self.initialPath.comp self.arrow.toPath
• initialPath_length : self.initialPath.length + 1 = arm.steps
• first_valid : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow self.arrow)))

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.firstArrowData {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) (hpos : 0 < arm.steps) : arm.FirstArrowData

Extract the boundary-adjacent arrow of a nonempty negative extension.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.positiveWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C D : Word R} (arm : C.NegativeExtension D) : Word R

Read the ordinary path of a negative extension as a positive string word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.positiveWord_eq_of_vertexBoundary_steps_eq {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) (C : Word P.relations) {z : Q} (a : C.target ⟶ z) (ha : IsString P.relations (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (haVertex : IsString P.relations (Quiver.Path.comp (vertex P.relations ⋯ C.target).path (Quiver.Hom.toPath (positiveArrow a)))) {D₁ D₂ : Word P.relations} (tail₁ : (append P.relations C (positiveArrow a) ha).NegativeExtension D₁) (tail₂ : (append P.relations (vertex P.relations ⋯ C.target) (positiveArrow a) haVertex).NegativeExtension D₂) (hsteps : tail₁.steps = tail₂.steps) : positiveWord ⋯ tail₁ = positiveWord ⋯ tail₂

Two equal-length negative tails after the same displayed positive arrow have the same positive word, even when the preceding base word differs. It is enough here to compare an arbitrary base with the trivial base used for the canonical hook.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.CanonicalAtArrow {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) (a : (y : Q) × (x : Q) × (x ⟶ y)) : Type u

A canonical maximal hook based at the trivial word of a displayed arrow's source.

• result : Word P.relations
• hook : (Word.vertex P.relations ⋯ a.snd.fst).HookExtension self.result
• boundary : ⟨self.hook.vertex, self.hook.arrow⟩ = ⟨a.fst, a.snd.snd⟩

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.canonicalAtArrow {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) (a : (y : Q) × (x : Q) × (x ⟶ y)) : CanonicalAtArrow P a

Choose the canonical-base maximal hook belonging to a displayed arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.canonicalKernelWord {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) (a : (y : Q) × (x : Q) × (x ⟶ y)) : Word P.relations

The positive tail word canonically determined by a displayed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.tail_positiveWord_eq_canonicalKernelWord {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) {C D : Word P.relations} (hook : C.HookExtension D) : NegativeExtension.positiveWord ⋯ hook.tail = canonicalKernelWord P ⟨hook.vertex, ⟨C.target, hook.arrow⟩⟩

The tail word of any maximal hook is the canonical word of its displayed boundary arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.displayedArrow_transport_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (h : C = C') (hook : C.HookExtension D) : have transported := ⋯.mp hook; ⟨transported.vertex, ⟨C'.target, transported.arrow⟩⟩ = ⟨hook.vertex, ⟨C.target, hook.arrow⟩⟩

Transporting the source word of a hook does not alter its displayed arrow.