Maximality obstructions for right-hook and right-cohook factorizations

A selected full-source-support component through a word longer than the complete hook must have an incoming boundary edge. At the hook endpoint, path transfer contradicts maximality directly. At the inherited source endpoint, factorization alignment transfers that edge through the second component and forces the first component to occupy two incompatible adjacent positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.not_length_lt_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (houtput : second.HasFullOutputSupport) (hinput : first.HasFullInputSupport) (hne : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) (hlength : length R D < length R M) : False

A component pair selected from a right-hook factorization cannot make the first component cover the complete hook inside a strictly longer word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_component_pair {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) (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (hfirstCoefficient : D.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0) (hsecondCoefficient : M.morphismCoefficientAt C hmono hmono g (↑second).representative ≠ 0) (hne : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A single component pair contributing nontrivially to the canonical right-hook component already forces one of the two ambient factor maps to split. In particular, the composite of the ambient maps need not equal the hook map; this is the form used after expanding a factorization through a finite direct sum of string modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_moduleMap_factorization {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) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.not_length_lt_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D) (hinput : first.HasFullInputSupport) (houtput : second.HasFullOutputSupport) (hne : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) (hlength : length R D < length R M) : False

A component pair selected from a right-cohook factorization cannot make the second component cover the complete cohook inside a strictly longer word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_component_pair {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) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D) (hfirstCoefficient : C.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0) (hsecondCoefficient : M.morphismCoefficientAt D hmono hmono g (↑second).representative ≠ 0) (hne : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A single component pair contributing nontrivially to the canonical right-cohook component already forces one of the two ambient factor maps to split. This is the direct-sum-ready form of cohook maximality.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_moduleMap_factorization {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) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

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