String maps controlled by the first extension letter

For an arbitrary right extension, the first new letter controls the module map across the old/new coordinate boundary. A negative first letter makes the old positions a subrepresentation, while a positive first letter makes their coordinate projection a quotient representation. Later letters may have either sign.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.exists_old_of_arrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {x y : Q} (b : x ⟶ y) (i : C.PositionAt x) (l : D.PositionAt y) (hil : D.ArrowStep b (extension.toRightExtension.position i) l) : ∃ (j : C.PositionAt y), extension.toRightExtension.position j = l

If the first appended letter is negative, every displayed-arrow output from an inherited position is still inherited, even after an arbitrary further tail.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.spaceInclusion_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {x y : Q} (b : x ⟶ y) (v : C.Space x) : (extension.toRightExtension.spaceInclusion y) ((C.arrowLinearMap b) v) = (D.arrowLinearMap b) ((extension.toRightExtension.spaceInclusion x) v)

The coordinate inclusion for a negative-boundary extension commutes with every displayed-arrow action.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.quiverRepresentationInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : C.quiverRepresentation ⟶ D.quiverRepresentation

A negative-boundary prefix inclusion is a morphism of quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.freeRightModuleAuxInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : D.freeRightModuleAux ⟶ C.freeRightModuleAux

In the opposite-module realization, the negative-boundary inclusion has the reversed natural-transformation direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.quotientRightModuleAuxInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) : D.quotientRightModuleAux hmono ⟶ C.quotientRightModuleAux hmono

Descend the negative-boundary inclusion through the monomial relation quotient.

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

The canonical inclusion associated to any extension whose first letter is negative, as a morphism of right modules.

@[simp]

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

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusion_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) : CategoryTheory.Mono (extension.rightModuleInclusion hmono)

A negative-boundary map is a submodule inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusion_transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.NegativeBoundaryExtension D) (second : D.NegativeBoundaryExtension E) (hmono : IsMonomial R) : (first.transRightExtension second.toRightExtension).rightModuleInclusion hmono = CategoryTheory.CategoryStruct.comp (first.rightModuleInclusion hmono) (second.rightModuleInclusion hmono)

Negative-boundary inclusions compose under further negative-boundary extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.not_arrowStep_to_old_of_not_old {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {x y : Q} (b : x ⟶ y) (j : D.PositionAt x) (i : C.PositionAt y) (hj : ¬∃ (q : C.PositionAt x), extension.toRightExtension.position q = j) : ¬D.ArrowStep b j (extension.toRightExtension.position i)

If the first appended letter is positive, no arrow action can travel from a non-inherited position back into an inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.spaceProjection_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {x y : Q} (b : x ⟶ y) (v : D.Space x) : (extension.toRightExtension.spaceProjection y) ((D.arrowLinearMap b) v) = (C.arrowLinearMap b) ((extension.toRightExtension.spaceProjection x) v)

The coordinate projection for a positive-boundary extension commutes with every displayed-arrow action.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.quiverRepresentationProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : D.quiverRepresentation ⟶ C.quiverRepresentation

A positive-boundary coordinate projection is a morphism of quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.freeRightModuleAuxProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : C.freeRightModuleAux ⟶ D.freeRightModuleAux

In the opposite-module realization, the positive-boundary projection has the reversed natural-transformation direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.quotientRightModuleAuxProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) : C.quotientRightModuleAux hmono ⟶ D.quotientRightModuleAux hmono

Descend the positive-boundary projection through the monomial relation quotient.

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

The canonical projection associated to any extension whose first letter is positive, as a morphism of right modules.

@[simp]

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

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjection_epi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) : CategoryTheory.Epi (extension.rightModuleProjection hmono)

A positive-boundary map is a quotient projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjection_transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.PositiveBoundaryExtension D) (second : D.PositiveBoundaryExtension E) (hmono : IsMonomial R) : (first.transRightExtension second.toRightExtension).rightModuleProjection hmono = CategoryTheory.CategoryStruct.comp (second.rightModuleProjection hmono) (first.rightModuleProjection hmono)

Positive-boundary projections compose under further positive-boundary extension.