Deleting maximal cohooks from string endpoints

In Butler--Ringel's peak cases, the endpoint operation is not a new hook: the given word is already a maximal cohook extension of a shorter word, and the cohook is deleted. This file packages that relation in the direction used by right-module Auslander--Reiten sequences. Its canonical map goes from the shortened word into the original word and is therefore the existing negative-boundary inclusion.

The left-hand construction is defined on reversed words but exposes maps and positions in the original orientation.

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

Deleting a maximal cohook at the right endpoint of C produces D. Equivalently, C is a maximal right cohook extension of D.

• cohook : D.CohookExtension C

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

The number of letters removed by a right cohook deletion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookDeletion.steps_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) : 0 < deletion.steps

A right cohook deletion removes a nonempty terminal segment.

@[simp]

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

Reattaching the deleted cohook recovers the original word length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookDeletion.source_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) : C.StartsOnPeak

A word from which a right cohook can be deleted starts on a peak at that endpoint.

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

The shortened word is not already in a deep at the deletion endpoint.

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

Embed an occurrence of the shortened word into the original word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookDeletion.position_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) {x : Q} (i : D.PositionAt x) : (deletion.position i).index = i.index

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

The canonical right-module map associated to deleting a right cohook.

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

@[simp]

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

The right-cohook deletion map sends every basis vector to the inherited position of the original word.

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

Deleting a maximal cohook at the left endpoint of C produces D. After reversing both words this is an ordinary right cohook deletion.

• cohook : (reverse R D).CohookExtension (reverse R C)

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookDeletion.toReverseLeftCohookDeletion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) : (reverse R C).LeftCohookDeletion (reverse R D)

Reversal turns a right cohook deletion into a left cohook deletion of the reversed word.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.toReverseDeletion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : (reverse R C).CohookDeletion (reverse R D)

The underlying right cohook deletion after reversing both words.

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

Regard a left cohook deletion as the corresponding negative left boundary extension of the shortened word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.toLeftNegativeBoundaryExtension_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : deletion.toLeftNegativeBoundaryExtension.result = C

The left-boundary extension associated to a deletion recovers the source word literally up to the canonical double-reversal equality.

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

The number of letters removed by a left cohook deletion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.steps_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : 0 < deletion.steps

A left cohook deletion removes a nonempty initial segment.

@[simp]

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

Reattaching the deleted left cohook recovers the original word length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.source_endsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : C.EndsOnPeak

A word from which a left cohook can be deleted ends on a peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.result_not_endsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : ¬D.EndsInDeep

The shortened word does not already end in a deep.

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

Embed an occurrence of the shortened word into the original word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.position_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) {x : Q} (i : D.PositionAt x) : (deletion.position i).index = deletion.steps + i.index

The inherited positions are shifted by the number of letters deleted on the left.

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

The canonical right-module map associated to deleting a left cohook.

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

@[simp]

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

The left-cohook deletion map sends every basis vector to the inherited position of the original word.