Testing irreducibility on indecomposable intermediate factors #
theorem
MagnitudeConjecture.CategoryTheory.retraction_ne_zero_of_ne_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{X Y : C}
(f : X ⟶ Y)
(hf : f ≠ 0)
[CategoryTheory.IsSplitMono f]
:
CategoryTheory.retraction f ≠ 0
theorem
MagnitudeConjecture.CategoryTheory.section_ne_zero_of_ne_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{X Y : C}
(f : X ⟶ Y)
(hf : f ≠ 0)
[CategoryTheory.IsSplitEpi f]
:
CategoryTheory.section_ f ≠ 0
theorem
MagnitudeConjecture.CategoryTheory.irreducible_of_indecomposable_factors
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(decomposition : ∀ (M : C), Nonempty (FiniteIndecomposableDecomposition M))
{X Y : C}
(f : X ⟶ Y)
(hf : f ≠ 0)
(hm : ¬CategoryTheory.IsSplitMono f)
(he : ¬CategoryTheory.IsSplitEpi f)
(hpair :
∀ (M : C),
CategoryTheory.Indecomposable M →
∀ (a : X ⟶ M) (b : M ⟶ Y), a ≠ 0 → b ≠ 0 → CategoryTheory.IsSplitMono a ∨ CategoryTheory.IsSplitEpi b)
:
With finite indecomposable decompositions, it suffices to test nonzero two-sided interactions with indecomposable intermediate objects.