Left-end hooks and cohooks for string modules

Butler--Ringel's canonical exact sequences use hook and cohook operations at both ends of a string. Reversal exchanges the two endpoints, so the left-end operations are obtained from the already constructed right-end operations. The module maps are transported through the canonical reversal isomorphisms; no second coordinate calculation is needed.

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

A maximal hook at the left endpoint. Its auxiliary result is stored in reversed orientation so that the underlying right hook is literal.

• reverseResult : Word R
• hook : (reverse R C).HookExtension self.reverseResult

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

The result word in the original orientation.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.toLeftPositiveBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) : C.LeftPositiveBoundaryExtension

Forget maximality while retaining the positive left boundary.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.asReverseHookEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.LeftHookExtension ≃ (D : Word R) × (reverse R C).HookExtension D

Left hooks are exactly right hooks on the reversed source word, with the auxiliary result retained in reversed orientation.

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

Every valid positive boundary at the reversed right endpoint gives a maximal hook at the original left endpoint.

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

The number of letters added by a left hook.

@[simp]

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

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

The canonical left-hook projection, transported through word reversal.

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

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) {x : Q} (i : C.PositionAt x) : hook.result.PositionAt x

Embed an occurrence of the original word into the result of a left hook. In reversed orientation this is the ordinary prefix-position embedding.

@[simp]

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

The left-hook projection is the identity on every inherited position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.not_endsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) : ¬C.EndsOnPeak

A left hook witnesses that the original word does not end on a peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.result_eq_of_boundary_eq {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (hook₁ hook₂ : C.LeftHookExtension) (hboundary : ⟨hook₁.hook.vertex, hook₁.hook.arrow⟩ = ⟨hook₂.hook.vertex, hook₂.hook.arrow⟩) : hook₁.result = hook₂.result

In a special-biserial presentation, the result of a left hook is uniquely determined by its reversed positive boundary arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.boundaryEquiv {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (C : Word P.relations) : C.LeftHookExtension ≃ (reverse P.relations C).PositiveAppendArrow

Maximal left hooks are in bijection with the valid positive boundary arrows at the reversed right endpoint.

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

A maximal cohook at the left endpoint. Its auxiliary result is stored in reversed orientation so that the underlying right cohook is literal.

• reverseResult : Word R
• cohook : (reverse R C).CohookExtension self.reverseResult

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

The result word in the original orientation.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.toLeftNegativeBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) : C.LeftNegativeBoundaryExtension

Forget maximality while retaining the negative left boundary.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.asReverseCohookEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.LeftCohookExtension ≃ (D : Word R) × (reverse R C).CohookExtension D

Left cohooks are exactly right cohooks on the reversed source word, with the auxiliary result retained in reversed orientation.

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

Every valid negative boundary at the reversed right endpoint gives a maximal cohook at the original left endpoint.

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

The number of letters added by a left cohook.

@[simp]

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

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

The canonical left-cohook inclusion, transported through word reversal.

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

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) {x : Q} (i : C.PositionAt x) : cohook.result.PositionAt x

Embed an occurrence of the original word into the result of a left cohook. In reversed orientation this is the ordinary prefix-position embedding.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_app_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (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.position i) c

The left-cohook inclusion carries every original position basis vector to its inherited position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.not_endsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) : ¬C.EndsInDeep

A left cohook witnesses that the original word does not end in a deep.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.result_eq_of_boundary_eq {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (cohook₁ cohook₂ : C.LeftCohookExtension) (hboundary : ⟨cohook₁.cohook.vertex, cohook₁.cohook.arrow⟩ = ⟨cohook₂.cohook.vertex, cohook₂.cohook.arrow⟩) : cohook₁.result = cohook₂.result

In a special-biserial presentation, the result of a left cohook is uniquely determined by its reversed negative boundary arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.boundaryEquiv {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (C : Word P.relations) : C.LeftCohookExtension ≃ (reverse P.relations C).NegativeAppendArrow

Maximal left cohooks are in bijection with the valid negative boundary arrows at the reversed right endpoint.