One-letter extension maps for string modules

The coordinate maps for one-letter string extensions already form morphisms of quiver representations. This file transports them through the free linear path realization and the monomial relation quotient, producing actual morphisms of right modules over the bound-quiver category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendFreeRightModuleAuxInclusionNegative {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)))) : (append R C (negativeArrow a) h).freeRightModuleAux ⟶ C.freeRightModuleAux

In the opposite-module realization, a negative one-letter inclusion has the reversed natural-transformation direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendFreeRightModuleAuxProjectionPositive {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)))) : C.freeRightModuleAux ⟶ (append R C (positiveArrow a) h).freeRightModuleAux

In the opposite-module realization, a positive one-letter projection has the reversed natural-transformation direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendQuotientRightModuleAuxInclusionNegative {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)))) (hmono : IsMonomial R) : (append R C (negativeArrow a) h).quotientRightModuleAux hmono ⟶ C.quotientRightModuleAux hmono

The negative-extension transformation descends through the monomial relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendQuotientRightModuleAuxProjectionPositive {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)))) (hmono : IsMonomial R) : C.quotientRightModuleAux hmono ⟶ (append R C (positiveArrow a) h).quotientRightModuleAux hmono

The positive-extension transformation descends through the monomial relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleInclusionNegative {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)))) (hmono : IsMonomial R) : C.rightModule hmono ⟶ (append R C (negativeArrow a) h).rightModule hmono

The canonical negative-extension inclusion as a morphism of right modules over the bound-quiver category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleProjectionPositive {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)))) (hmono : IsMonomial R) : (append R C (positiveArrow a) h).rightModule hmono ⟶ C.rightModule hmono

The canonical positive-extension projection as a morphism of right modules over the bound-quiver category.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleInclusionNegative_app_obj {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)))) (hmono : IsMonomial R) (x : Q) : (C.appendRightModuleInclusionNegative a h hmono).app (Opposite.op (obj R x)) = ModuleCat.ofHom (C.appendSpaceInclusion (negativeArrow a) h)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleProjectionPositive_app_obj {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)))) (hmono : IsMonomial R) (x : Q) : (C.appendRightModuleProjectionPositive a h hmono).app (Opposite.op (obj R x)) = ModuleCat.ofHom (C.appendSpaceProjection (positiveArrow a) h)

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleInclusionNegative_mono {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)))) (hmono : IsMonomial R) : CategoryTheory.Mono (C.appendRightModuleInclusionNegative a h hmono)

The negative one-letter map is a submodule inclusion.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.appendRightModuleProjectionPositive_epi {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)))) (hmono : IsMonomial R) : CategoryTheory.Epi (C.appendRightModuleProjectionPositive a h hmono)

The positive one-letter map is a quotient projection.