Boundary extensions at the left endpoint of a string

Reversal turns a left extension into an ordinary right extension. This file packages that transport before imposing the maximal-tail conditions defining hooks and cohooks. It also exposes the resulting maps on the original position basis, so left- and right-endpoint maps can be combined in the same coordinate argument.

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

A nonempty left extension whose boundary letter becomes positive after reversing the source word.

• reverseResult : Word R
• extension : (reverse R C).PositiveBoundaryExtension self.reverseResult

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

The extended word in the original orientation.

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

Number of letters added at the left endpoint.

@[simp]

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

A left extension increases the word length by its number of added letters.

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

The canonical left-boundary quotient map, transported through word reversal.

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

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

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

@[simp]

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

Embedding an old position into a left extension shifts its index by the number of letters added on the left.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.exists_eq_position_of_steps_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (j : extension.result.PositionAt x) (hj : extension.steps ≤ j.index) : ∃ (i : C.PositionAt x), extension.position i = j

Every position at or to the right of the first inherited index in a left extension comes from the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (x : Q) : extension.result.Space x →ₗ[k] C.Space x

Coordinate projection from a left-extended word onto its inherited positions, expressed by reversal and the ordinary right-extension projection.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (x : Q) : C.Space x →ₗ[k] extension.result.Space x

Coordinate inclusion of the inherited positions into a left positive boundary extension. This is a linear splitting of the canonical projection, although it is not generally a module morphism.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMap_app_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) (x : Q) : (extension.moduleMap hmono).app (Opposite.op (obj R x)) = ModuleCat.ofHom (extension.spaceProjection x)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.position_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} : Function.Injective extension.position

The inherited-position embedding of a left positive extension is injective.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceProjection_single_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceProjection x) (Finsupp.single (extension.position i) c) = Finsupp.single i c

The coordinate projection is the identity on inherited basis positions.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceInclusion_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceInclusion x) (Finsupp.single i c) = Finsupp.single (extension.position i) c

The coordinate inclusion sends a basis vector to its inherited position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceProjection_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (x : Q) (v : C.Space x) : (extension.spaceProjection x) ((extension.spaceInclusion x) v) = v

The left-boundary projection is a left inverse to its coordinate inclusion.

@[simp]

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

A left positive-boundary module projection is the identity on inherited basis positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceProjection_single_of_not_exists {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (j : extension.result.PositionAt x) (c : k) (hj : ¬∃ (i : C.PositionAt x), extension.position i = j) : (extension.spaceProjection x) (Finsupp.single j c) = 0

The left coordinate projection kills every basis position not inherited from the original word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.spaceProjection_apply_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (v : extension.result.Space x) (i : C.PositionAt x) : ((extension.spaceProjection x) v) i = v (extension.position i)

Projection reads the coefficient at the corresponding inherited position.

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

A nonempty left extension whose boundary letter becomes negative after reversing the source word.

• reverseResult : Word R
• extension : (reverse R C).NegativeBoundaryExtension self.reverseResult

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

The extended word in the original orientation.

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

Number of letters added at the left endpoint.

@[simp]

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

A negative left extension increases the word length by its number of added letters.

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

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

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

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

Embed an occurrence of the original word into the left-extended result.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.prefixPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) : SignedPath extension.result.source C.source

The signed prefix added before the original word, written in the original orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.path_cast_eq_prefixPath_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) : Quiver.Path.cast ⋯ ⋯ extension.result.path = Quiver.Path.comp extension.prefixPath C.path

After casting the preserved endpoint, a negative left extension is its added prefix followed by the original word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.path_eq_prefixPath_comp_cast {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) : extension.result.path = Quiver.Path.comp extension.prefixPath (Quiver.Path.cast ⋯ ⋯ C.path)

The same factorization with the original word cast to the actual right endpoint of the left extension.

@[simp]

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

Embedding an old position into a negative left extension shifts its index by the number of letters added on the left.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.exists_eq_position_of_steps_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (j : extension.result.PositionAt x) (hj : extension.steps ≤ j.index) : ∃ (i : C.PositionAt x), extension.position i = j

Every position at or to the right of the first inherited index in a negative left extension comes from the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (x : Q) : C.Space x →ₗ[k] extension.result.Space x

Coordinate inclusion for a negative left boundary, expressed by reversal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (x : Q) : extension.result.Space x →ₗ[k] C.Space x

Coordinate projection onto the inherited positions of a negative left extension. It is a linear retraction of spaceInclusion; unlike the latter, it is not generally a module morphism.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMap_app_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) (x : Q) : (extension.moduleMap hmono).app (Opposite.op (obj R x)) = ModuleCat.ofHom (extension.spaceInclusion x)

@[simp]

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

The left negative-boundary inclusion carries a basis vector to its inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.position_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} : Function.Injective extension.position

The inherited-position embedding of a negative left extension is injective.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceProjection_single_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceProjection x) (Finsupp.single (extension.position i) c) = Finsupp.single i c

The coordinate projection is the identity on inherited basis positions.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceInclusion_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceInclusion x) (Finsupp.single i c) = Finsupp.single (extension.position i) c

The negative left coordinate inclusion sends a basis vector to its inherited position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceProjection_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (x : Q) (v : C.Space x) : (extension.spaceProjection x) ((extension.spaceInclusion x) v) = v

The negative left coordinate projection retracts its inclusion.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceInclusion_apply_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (v : C.Space x) (i : C.PositionAt x) : ((extension.spaceInclusion x) v) (extension.position i) = v i

Inclusion preserves the coefficient at every inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceInclusion_apply_of_not_exists {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (v : C.Space x) (j : extension.result.PositionAt x) (hj : ¬∃ (i : C.PositionAt x), extension.position i = j) : ((extension.spaceInclusion x) v) j = 0

Inclusion has zero coefficient at every non-inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceProjection_single_of_not_exists {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (j : extension.result.PositionAt x) (c : k) (hj : ¬∃ (i : C.PositionAt x), extension.position i = j) : (extension.spaceProjection x) (Finsupp.single j c) = 0

The negative left coordinate projection kills basis positions which do not come from the shorter word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.spaceProjection_apply_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (v : extension.result.Space x) (i : C.PositionAt x) : ((extension.spaceProjection x) v) i = v (extension.position i)

Projection reads the coefficient at the corresponding inherited position.