Essential-image closure from almost-split morphisms

If the image of a morphism is right almost split, every irreducible predecessor of its endpoint is a retract of the image of its source. A finite indecomposable decomposition of that source and localness of the predecessor's endomorphism ring then identify the predecessor with the image of one indecomposable summand. The dual statement uses a left almost-split image.

These are the categorical component-closure steps in Gabriel's Theorem 3.6(b).

theorem MagnitudeConjecture.CategoryTheory.exists_iso_finBiproduct_summand_of_isSplitMono {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] {J : Type} [Fintype J] (X : J → D) (hX : ∀ (j : J), CategoryTheory.Indecomposable (X j)) {Y : D} (hY : CategoryTheory.Indecomposable Y) [IsLocalRing (CategoryTheory.End Y)] (f : Y ⟶ ⨁ X) [CategoryTheory.IsSplitMono f] : ∃ (j : J), Nonempty (Y ≅ X j)

A split subobject of a finite biproduct of indecomposables is isomorphic to one of its summands when the source is indecomposable with local endomorphism ring.

theorem MagnitudeConjecture.CategoryTheory.exists_essentialImage_of_irreducible_to_of_map_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] (F : CategoryTheory.Functor C D) [F.Additive] (decomposition : ∀ (Z : C), Nonempty (FiniteIndecomposableDecomposition Z)) (map_indec : ∀ (Z : C), CategoryTheory.Indecomposable Z → CategoryTheory.Indecomposable (F.obj Z)) {M N : C} (m : N ⟶ M) (hm : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (F.map m)) {Y : D} (hY : CategoryTheory.Indecomposable Y) (hlocalY : IsLocalRing (CategoryTheory.End Y)) (f : Y ⟶ F.obj M) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ∃ (Z : C), CategoryTheory.Indecomposable Z ∧ Nonempty (F.obj Z ≅ Y)

If F.map m is right almost split, every irreducible predecessor of its endpoint belongs to the essential image of F, provided the source of m has a finite indecomposable decomposition and F preserves those indecomposables.

theorem MagnitudeConjecture.CategoryTheory.exists_essentialImage_of_irreducible_from_of_map_leftAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] (F : CategoryTheory.Functor C D) [F.Additive] (decomposition : ∀ (Z : C), Nonempty (FiniteIndecomposableDecomposition Z)) (map_indec : ∀ (Z : C), CategoryTheory.Indecomposable Z → CategoryTheory.Indecomposable (F.obj Z)) {M N : C} (m : M ⟶ N) (hm : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (F.map m)) {Y : D} (hY : CategoryTheory.Indecomposable Y) (hlocalY : IsLocalRing (CategoryTheory.End Y)) (f : F.obj M ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ∃ (Z : C), CategoryTheory.Indecomposable Z ∧ Nonempty (F.obj Z ≅ Y)

Dual component closure: if F.map m is left almost split, every irreducible successor of its source belongs to the essential image of F.