One-letter extensions of string words

Appending one signed arrow adds exactly one endpoint occurrence to the word. This file constructs the embedding of all old prefix positions into the extended word and the induced linear inclusion and projection on vertex spaces. These are the coordinate maps underlying the canonical hook and cohook morphisms.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : C.PositionAt x) : (append R C e h).PositionAt x

Every old prefix position remains a prefix position after one letter is appended.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendPosition_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : C.PositionAt x) : ↑(C.appendPosition e h i) = ↑i

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : C.PositionAt x) : (C.appendPosition e h i).index = i.index

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendPosition_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : Function.Injective (C.appendPosition e h)

Appending positions is injective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowStep_appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : (append R C e h).ArrowStep a (C.appendPosition e h i) (C.appendPosition e h j)

Every arrow step between old positions remains an arrow step after appending a letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (p : Quiver.Path x y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.PathReach p i j) : (append R C e h).PathReach p (C.appendPosition e h i) (C.appendPosition e h j)

Path reachability between old positions is preserved by appending a letter.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendEndPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : (append R C e h).PositionAt z

The new final occurrence of the appended word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendEndPosition_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : ↑(C.appendEndPosition e h) = (append R C e h).path

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendEndPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : (C.appendEndPosition e h).index = length R C + 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_eq_appendPosition_of_index_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (j : (append R C e h).PositionAt x) (hj : j.index ≤ length R C) : ∃ (i : C.PositionAt x), C.appendPosition e h i = j

A position in the appended word whose index has not passed the old final index comes from a unique old position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_appendEndPosition_of_not_exists_old {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (j : (append R C e h).PositionAt z) (hj : ¬∃ (i : C.PositionAt z), C.appendPosition e h i = j) : j = C.appendEndPosition e h

The final endpoint is the only position created by appending one letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_exists_appendPosition_eq_appendEndPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : ¬∃ (i : C.PositionAt z), C.appendPosition e h i = C.appendEndPosition e h

The new endpoint is not the image of an old position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_old_of_arrowStep_appendPosition_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) (b : x ⟶ y) (i : C.PositionAt x) (l : (append R C (negativeArrow a) h).PositionAt y) (hil : (append R C (negativeArrow a) h).ArrowStep b (C.appendPosition (negativeArrow a) h i) l) : ∃ (j : C.PositionAt y), C.appendPosition (negativeArrow a) h j = l

Appending a negative letter creates no new arrow output from an old position. The new endpoint is a source for the underlying displayed arrow, not a target of an old basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_exists_arrowStep_appendEndPosition_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z y : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (b : z ⟶ y) : ¬∃ (l : (append R C (positiveArrow a) h).PositionAt y), (append R C (positiveArrow a) h).ArrowStep b (C.appendEndPosition (positiveArrow a) h) l

After appending a positive letter, the new endpoint has no outgoing displayed-arrow step.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : C.Space x →ₗ[k] (append R C e h).Space x

The old-position inclusion on a vertex space.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceInclusion_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : C.PositionAt x) (c : k) : (C.appendSpaceInclusion e h) (Finsupp.single i c) = Finsupp.single (C.appendPosition e h i) c

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : (append R C e h).Space x →ₗ[k] C.Space x

The coordinate projection from an appended vertex space onto its old positions. The unique new endpoint basis vector is sent to zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_single_of_not_exists_old {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (j : (append R C e h).PositionAt x) (c : k) (hj : ¬∃ (i : C.PositionAt x), C.appendPosition e h i = j) : (C.appendSpaceProjection e h) (Finsupp.single j c) = 0

Projection kills a basis position which is not inherited from the old word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_single_appendEndPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (c : k) : (C.appendSpaceProjection e h) (Finsupp.single (C.appendEndPosition e h) c) = 0

In particular, projection kills the newly appended endpoint.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_single_appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : C.PositionAt x) (c : k) : (C.appendSpaceProjection e h) (Finsupp.single (C.appendPosition e h i) c) = Finsupp.single i c

Projection after inclusion is the identity on every old basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (v : C.Space x) : (C.appendSpaceProjection e h) ((C.appendSpaceInclusion e h) v) = v

Projection is a left inverse to the old-position inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceInclusion_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : Function.Injective ⇑(C.appendSpaceInclusion e h)

The old-position inclusion is injective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_surjective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) : Function.Surjective ⇑(C.appendSpaceProjection e h)

The old-coordinate projection is surjective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_arrowLinearMap_positive_appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (b : x ⟶ y) (i : C.PositionAt x) : (C.appendSpaceProjection (positiveArrow a) h) (((append R C (positiveArrow a) h).arrowLinearMap b) (Finsupp.single (C.appendPosition (positiveArrow a) h i) 1)) = (C.arrowLinearMap b) ((C.appendSpaceProjection (positiveArrow a) h) (Finsupp.single (C.appendPosition (positiveArrow a) h i) 1))

For a positive appended letter, projection commutes with displayed-arrow action on every inherited basis vector. A possible new target is precisely the appended endpoint and is therefore killed by projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_arrowLinearMap_positive_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (b : x ⟶ y) (j : (append R C (positiveArrow a) h).PositionAt x) : (C.appendSpaceProjection (positiveArrow a) h) (((append R C (positiveArrow a) h).arrowLinearMap b) (Finsupp.single j 1)) = (C.arrowLinearMap b) ((C.appendSpaceProjection (positiveArrow a) h) (Finsupp.single j 1))

For a positive appended letter, projection commutes with displayed-arrow action on every basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceProjection_arrowLinearMap_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (b : x ⟶ y) (v : (append R C (positiveArrow a) h).Space x) : (C.appendSpaceProjection (positiveArrow a) h) (((append R C (positiveArrow a) h).arrowLinearMap b) v) = (C.arrowLinearMap b) ((C.appendSpaceProjection (positiveArrow a) h) v)

Appending a positive letter makes the old coordinate projection a morphism of quiver representations.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceInclusion_arrowLinearMap_negative_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) (b : x ⟶ y) (i : C.PositionAt x) : (C.appendSpaceInclusion (negativeArrow a) h) ((C.arrowLinearMap b) (Finsupp.single i 1)) = ((append R C (negativeArrow a) h).arrowLinearMap b) ((C.appendSpaceInclusion (negativeArrow a) h) (Finsupp.single i 1))

For a negative appended letter, the old-position inclusion commutes with every displayed-arrow action on a basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendSpaceInclusion_arrowLinearMap_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z x y : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) (b : x ⟶ y) (v : C.Space x) : (C.appendSpaceInclusion (negativeArrow a) h) ((C.arrowLinearMap b) v) = ((append R C (negativeArrow a) h).arrowLinearMap b) ((C.appendSpaceInclusion (negativeArrow a) h) v)

Appending a negative letter makes the old coordinate spaces a subrepresentation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendQuiverRepresentationInclusionNegative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) : C.quiverRepresentation ⟶ (append R C (negativeArrow a) h).quiverRepresentation

The canonical inclusion associated to a negative one-letter extension, packaged as a morphism of quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendQuiverRepresentationProjectionPositive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) : (append R C (positiveArrow a) h).quiverRepresentation ⟶ C.quiverRepresentation

The canonical projection associated to a positive one-letter extension, packaged as a morphism of quiver representations.