Strict hook and cohook morphisms

Every hook or cohook adds at least one word position. The canonical hook projection kills a new position, while the canonical cohook inclusion misses one. Thus the four right-module maps at the two word endpoints are proper epimorphisms or proper monomorphisms. String-module indecomposability then rules out a splitting in the other direction as well.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.not_exists_position_targetPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (hsteps : extension.steps ≠ 0) : ¬∃ (i : C.PositionAt D.target), extension.position i = D.targetPosition

The final position of a nontrivial right extension is not inherited from the original word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_not_surjective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (hsteps : extension.steps ≠ 0) : ¬Function.Surjective ⇑(extension.spaceInclusion D.target)

The coordinate inclusion of a nontrivial right extension misses its new final position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_not_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (hsteps : extension.steps ≠ 0) : ¬Function.Injective ⇑(extension.spaceProjection D.target)

The coordinate projection of a nontrivial right extension kills its new final basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.not_exists_position_sourcePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) : ¬∃ (i : C.PositionAt extension.result.source), extension.position i = extension.result.sourcePosition

The source position of a nontrivial left extension is not inherited from the original word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.not_exists_position_sourcePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) : ¬∃ (i : C.PositionAt extension.result.source), extension.position i = extension.result.sourcePosition

The source position of a nontrivial negative left extension is not inherited from the original word.

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

A negative right-boundary inclusion is a proper monomorphism.

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

A positive right-boundary projection is a proper epimorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMap_not_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) : ¬CategoryTheory.Mono (extension.moduleMap hmono)

A positive left-boundary projection is a proper epimorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMap_not_epi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : ¬CategoryTheory.Epi (extension.moduleMap hmono)

A negative left-boundary inclusion is a proper monomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.moduleMap_not_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.Mono (hook.moduleMap hmono)

A right hook projection is not monic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.moduleMap_not_isSplitMono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitMono (hook.moduleMap hmono)

A right hook projection is not split monic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.moduleMap_not_isSplitEpi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitEpi (hook.moduleMap hmono)

A right hook projection is not split epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_not_epi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.Epi (cohook.moduleMap hmono)

A right cohook inclusion is not epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_not_isSplitEpi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitEpi (cohook.moduleMap hmono)

A right cohook inclusion is not split epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_not_isSplitMono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitMono (cohook.moduleMap hmono)

A right cohook inclusion is not split monic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMap_not_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.Mono (hook.moduleMap hmono)

A left hook projection is not monic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMap_not_isSplitMono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitMono (hook.moduleMap hmono)

A left hook projection is not split monic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMap_not_isSplitEpi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitEpi (hook.moduleMap hmono)

A left hook projection is not split epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_not_epi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.Epi (cohook.moduleMap hmono)

A left cohook inclusion is not epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_not_isSplitEpi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitEpi (cohook.moduleMap hmono)

A left cohook inclusion is not split epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_not_isSplitMono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : ¬CategoryTheory.IsSplitMono (cohook.moduleMap hmono)

A left cohook inclusion is not split monic.