Reversal of string representations

A prefix occurrence in a word becomes the reversed complementary suffix in the reversed word. This file begins the explicit reversal equivalence needed to transport right-endpoint hook and cohook constructions to the left endpoint.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.suffix {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} (i : C.PositionAt x) : SignedPath x C.target

The complementary suffix belonging to a prefix position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.prefix_comp_suffix {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} (i : C.PositionAt x) : C.path = Quiver.Path.comp (↑i) i.suffix

A position prefix followed by its chosen suffix recovers the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.suffix_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} (i : C.PositionAt x) : Quiver.Path.length i.suffix = length R C - i.index

The suffix length is the complementary word index.

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

Reverse a prefix position by taking the reverse of its complementary suffix.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reversePosition_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i : C.PositionAt x) : ↑(C.reversePosition i) = Quiver.Path.reverse i.suffix

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reversePosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i : C.PositionAt x) : (C.reversePosition i).index = length R C - i.index

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.unreversePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (j : (reverse R C).PositionAt x) : C.PositionAt x

Undo reversal of a prefix position without casting through the bundled identity C.reverse.reverse = C.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.unreversePosition_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (j : (reverse R C).PositionAt x) : ↑(C.unreversePosition j) = Quiver.Path.reverse j.suffix

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.unreversePosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (j : (reverse R C).PositionAt x) : (C.unreversePosition j).index = length R C - j.index

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reversePositionEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : C.PositionAt x ≃ (reverse R C).PositionAt x

Prefix occurrences at every displayed vertex are canonically equivalent under word reversal.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowStep_reversePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : (reverse R C).ArrowStep a (C.reversePosition i) (C.reversePosition j)

Reversal preserves the displayed-arrow adjacency relation on prefix occurrences.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowStep_unreversePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (i : (reverse R C).PositionAt x) (j : (reverse R C).PositionAt y) (hij : (reverse R C).ArrowStep a i j) : C.ArrowStep a (C.unreversePosition i) (C.unreversePosition j)

The inverse position map also preserves displayed-arrow adjacency.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseSpaceEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : C.Space x ≃ₗ[k] (reverse R C).Space x

Reindex the position basis of a string word by reversed occurrences.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseSpaceEquiv_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i : C.PositionAt x) (c : k) : (C.reverseSpaceEquiv x) (Finsupp.single i c) = Finsupp.single (C.reversePosition i) c

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseSpaceEquiv_symm_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (j : (reverse R C).PositionAt x) (c : k) : (C.reverseSpaceEquiv x).symm (Finsupp.single j c) = Finsupp.single (C.unreversePosition j) c

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseSpaceEquiv_arrowLinearMap_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) : (C.reverseSpaceEquiv y) ((C.arrowLinearMap a) (Finsupp.single i 1)) = ((reverse R C).arrowLinearMap a) ((C.reverseSpaceEquiv x) (Finsupp.single i 1))

Reversal reindexing commutes with every displayed-arrow action on a basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseSpaceEquiv_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (v : C.Space x) : (C.reverseSpaceEquiv y) ((C.arrowLinearMap a) v) = ((reverse R C).arrowLinearMap a) ((C.reverseSpaceEquiv x) v)

Reversal reindexing is a morphism of quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseQuiverRepresentationIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.quiverRepresentation ≅ (reverse R C).quiverRepresentation

A string word and its reverse carry canonically isomorphic quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseFreeRightModuleAuxIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : (reverse R C).freeRightModuleAux ≅ C.freeRightModuleAux

In the opposite-module realization, reversal gives an isomorphism in the opposite direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseQuotientRightModuleAuxIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (reverse R C).quotientRightModuleAux hmono ≅ C.quotientRightModuleAux hmono

The reversal isomorphism descends through a monomial relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseRightModuleIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.rightModule hmono ≅ (reverse R C).rightModule hmono

A string word and its reverse define canonically isomorphic right modules.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseRightModuleIso_hom_app_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (x : Q) : (C.reverseRightModuleIso hmono).hom.app (Opposite.op (obj R x)) = ModuleCat.ofHom ↑(C.reverseSpaceEquiv x)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reverseRightModuleIso_inv_app_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (x : Q) : (C.reverseRightModuleIso hmono).inv.app (Opposite.op (obj R x)) = ModuleCat.ofHom ↑(C.reverseSpaceEquiv x).symm