Maximal hooks and cohooks at string endpoints

This file records Butler--Ringel's endpoint terminology in the current word convention. At the right endpoint, a hook begins with a positive letter and continues along a negative arm until a deep is reached. A cohook begins with a negative letter and continues along a positive arm until a peak is reached.

Because the formalization uses right modules, the canonical hook map is the resulting quotient projection and the canonical cohook map is the resulting submodule inclusion. Reversal makes the same definitions available at the left endpoint.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.StartsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Prop

A word starts on a peak at its right endpoint when no positive displayed arrow can be appended while retaining the string condition.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.StartsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Prop

A word starts in a deep at its right endpoint when no negative displayed arrow can be appended while retaining the string condition.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.EndsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Prop

Left-end peak terminology, defined by reversal.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.EndsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Prop

Left-end deep terminology, defined by reversal.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverse_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : (reverse R C).StartsOnPeak ↔ C.EndsOnPeak

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverse_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : (reverse R C).StartsInDeep ↔ C.EndsInDeep

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverse_endsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : (reverse R C).EndsOnPeak ↔ C.StartsOnPeak

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverse_endsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : (reverse R C).EndsInDeep ↔ C.StartsInDeep

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_negativeExtension_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : ∃ (D : Word R) (_arm : C.NegativeExtension D), D.StartsInDeep

Admissibility ensures that every word has a maximal negative extension arm. No finiteness or uniqueness of the displayed arrows is needed.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_positiveExtension_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : ∃ (D : Word R) (_arm : C.PositiveExtension D), D.StartsOnPeak

Admissibility ensures that every word has a maximal positive extension arm.

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

A maximal right hook: append one positive letter and then a negative arm whose endpoint starts in a deep.

• vertex : Q
• arrow : C.target ⟶ self.vertex
• valid : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow self.arrow)))
• tail : (append R C (positiveArrow self.arrow) ⋯).NegativeExtension D
• maximal : D.StartsInDeep

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.exists_of_append_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) {z : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) : ∃ (D : Word R) (hook : C.HookExtension D), ⟨hook.vertex, hook.arrow⟩ = ⟨z, a⟩

Every valid initial positive letter extends to a maximal hook.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.toPositiveBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) : C.PositiveBoundaryExtension D

A hook is in particular an arbitrary extension with positive boundary.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) : ℕ

The number of letters appended by the hook.

@[simp]

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

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

The canonical right-module hook projection.

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.not_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) : ¬C.StartsOnPeak

The presence of a hook witnesses that the original word does not start on a peak.

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

A maximal right cohook: append one negative letter and then a positive arm whose endpoint starts on a peak.

• vertex : Q
• arrow : self.vertex ⟶ C.target
• valid : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow self.arrow)))
• tail : (append R C (negativeArrow self.arrow) ⋯).PositiveExtension D
• maximal : D.StartsOnPeak

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.exists_of_append_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) {z : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) : ∃ (D : Word R) (cohook : C.CohookExtension D), ⟨cohook.vertex, cohook.arrow⟩ = ⟨z, a⟩

Every valid initial negative letter extends to a maximal cohook.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.toNegativeBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) : C.NegativeBoundaryExtension D

A cohook is in particular an arbitrary extension with negative boundary.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) : ℕ

The number of letters appended by the cohook.

@[simp]

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

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

The canonical right-module cohook inclusion.

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

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_app_single_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) (c : k) : (CategoryTheory.ConcreteCategory.hom ((cohook.moduleMap hmono).app (Opposite.op (obj R x)))) (Finsupp.single i c) = Finsupp.single (cohook.toNegativeBoundaryExtension.toRightExtension.position i) c

The right-cohook inclusion carries an inherited basis vector to the corresponding prefix position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.not_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) : ¬C.StartsInDeep

The presence of a cohook witnesses that the original word does not start in a deep.