Literal factorization clauses at the left endpoint

Word reversal conjugates the left hook and cohook maps to the corresponding right-end maps. Their literal-string factorization clauses therefore transport through the canonical reversal isomorphisms without repeating the component-boundary argument.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.isSplitMono_or_isSplitEpi_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) (f : hook.result.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

Every factorization of a canonical left-hook projection through a literal string module has a split first factor or a split second factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.isSplitMono_or_isSplitEpi_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ cohook.result.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

Every factorization of a canonical left-cohook inclusion through a literal string module has a split first factor or a split second factor.