Hook and cohook factorizations through sums of string modules

A factorization through a finite biproduct is the sum of its factorizations through the individual summands. Since a canonical hook or cohook map has a nonzero coefficient on its distinguished graph component, one summand makes a nonzero contribution there. Component-pair maximality on that summand forces the original map into the biproduct to split monic or the original map out of it to split epic.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_biproduct_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) (f : D.rightModule hmono ⟶ ⨁ fun (i : ι) => (M i).rightModule hmono) (g : (⨁ fun (i : ι) => (M i).rightModule hmono) ⟶ C.rightModule hmono) (hcoefficient : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp f g) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

If a morphism through a finite biproduct of literal string modules has a nonzero coefficient on the distinguished component of a right hook, then its two factors cannot both be nonsplit.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) (f : D.rightModule hmono ⟶ ⨁ fun (i : ι) => (M i).rightModule hmono) (g : (⨁ fun (i : ι) => (M i).rightModule hmono) ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A right-hook factorization through a finite biproduct of literal string modules has a split first or second factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_biproduct_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) (f : C.rightModule hmono ⟶ ⨁ fun (i : ι) => (M i).rightModule hmono) (g : (⨁ fun (i : ι) => (M i).rightModule hmono) ⟶ D.rightModule hmono) (hcoefficient : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp f g) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

If a morphism through a finite biproduct of literal string modules has a nonzero coefficient on the distinguished component of a right cohook, then its two factors cannot both be nonsplit.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) (f : C.rightModule hmono ⟶ ⨁ fun (i : ι) => (M i).rightModule hmono) (g : (⨁ fun (i : ι) => (M i).rightModule hmono) ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A right-cohook factorization through a finite biproduct of literal string modules has a split first or second factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : D.rightModule hmono ⟶ N) (g : N ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A right-hook factorization through an object explicitly isomorphic to a finite biproduct of literal string modules has a split factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : D.rightModule hmono ⟶ N) (g : N ⟶ C.rightModule hmono) (hcoefficient : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp f g) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The distinguished-coefficient form of the right-hook factorization criterion is invariant under replacing the intermediate object by an isomorphic finite string sum.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : C.rightModule hmono ⟶ N) (g : N ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A right-cohook factorization through an object explicitly isomorphic to a finite biproduct of literal string modules has a split factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : C.rightModule hmono ⟶ N) (g : N ⟶ D.rightModule hmono) (hcoefficient : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp f g) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The distinguished-coefficient form of the right-cohook factorization criterion is invariant under replacing the intermediate object by an isomorphic finite string sum.

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

Reversal transports the finite-biproduct factorization clause to a left hook.

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

Reversal transports the finite-biproduct factorization clause to a left cohook.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : hook.result.rightModule hmono ⟶ N) (g : N ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A left-hook factorization through an object explicitly isomorphic to a finite biproduct of literal string modules has a split factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.isSplitMono_or_isSplitEpi_of_iso_biproduct_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) {ι : Type} [Fintype ι] (M : ι → Word R) {N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (e : N ≅ ⨁ fun (i : ι) => (M i).rightModule hmono) (f : C.rightModule hmono ⟶ N) (g : N ⟶ cohook.result.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

A left-cohook factorization through an object explicitly isomorphic to a finite biproduct of literal string modules has a split factor.