Equal-length branches of hook and cohook factorizations

The graph-component extraction retains nonzero coefficients of the actual factor maps. If the intermediate word has the same length as the old hook or cohook word, the selected one-sided full-support component is automatically two-sided, so the corresponding factor itself is an isomorphism. Thus a nonsplit factor forces strict growth of the intermediate word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.secondFactor_isIso_of_intermediate_length_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (f : D.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) (hlength : length R M = length R C) : CategoryTheory.IsIso g

In a right-hook factorization through an equal-length string, the second factor is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.base_length_lt_intermediate_of_not_isSplitEpi {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (f : D.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) (hg : ¬CategoryTheory.IsSplitEpi g) : length R C < length R M

A nonsplit second factor of a right hook must pass through a strictly longer intermediate string than the hook target.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.firstFactor_isIso_of_intermediate_length_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) (hlength : length R M = length R C) : CategoryTheory.IsIso f

In a right-cohook factorization through an equal-length string, the first factor is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.base_length_lt_intermediate_of_not_isSplitMono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) (hf : ¬CategoryTheory.IsSplitMono f) : length R C < length R M

A nonsplit first factor of a right cohook must pass through a strictly longer intermediate string than the cohook source.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.secondFactor_isIso_of_intermediate_length_eq {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) (hlength : length R M = length R C) : CategoryTheory.IsIso g

In a left-hook factorization through an equal-length string, the second factor is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.base_length_lt_intermediate_of_not_isSplitEpi {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) (hg : ¬CategoryTheory.IsSplitEpi g) : length R C < length R M

A nonsplit second factor of a left hook must pass through a strictly longer intermediate string than the hook target.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.firstFactor_isIso_of_intermediate_length_eq {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) (hlength : length R M = length R C) : CategoryTheory.IsIso f

In a left-cohook factorization through an equal-length string, the first factor is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.base_length_lt_intermediate_of_not_isSplitMono {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) (hf : ¬CategoryTheory.IsSplitMono f) : length R C < length R M

A nonsplit first factor of a left cohook must pass through a strictly longer intermediate string than the cohook source.