Irreducible components of minimal almost-split morphisms

This leaf module keeps the finite Krull--Schmidt matrix dependency out of the widely imported elementary irreducible-morphism API.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.irreducible_comp_of_splitSummand {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X E Z : C} (g : E ⟶ Z) (hg : IsRightAlmostSplit g) (hgmin : IsRightMinimal g) (inc : X ⟶ E) (proj : E ⟶ X) (hinc : CategoryTheory.CategoryStruct.comp inc proj = CategoryTheory.CategoryStruct.id X) (hX : CategoryTheory.Indecomposable X) (hZ : CategoryTheory.Indecomposable Z) : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp inc g)

A component cut out by an indecomposable split summand from a minimal right almost-split morphism to an indecomposable target is irreducible.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.comp_irreducible_of_splitSummand {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X E Y : C} (f : X ⟶ E) (hf : IsLeftAlmostSplit f) (hfmin : IsLeftMinimal f) (proj : E ⟶ Y) (inc : Y ⟶ E) (hinc : CategoryTheory.CategoryStruct.comp inc proj = CategoryTheory.CategoryStruct.id Y) (hX : CategoryTheory.Indecomposable X) (hY : CategoryTheory.Indecomposable Y) : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp f proj)

A component cut out by an indecomposable split quotient of the target of a minimal left almost-split morphism from an indecomposable source is irreducible.