Irreducible morphisms in an abelian category

The canonical epi--mono image factorization shows that an irreducible morphism in an abelian category is either monic or epic. This is the categorical step used in Ringel's support argument for an almost-split sequence.

theorem QuotientSubmoduleEquidistribution.IsIrreducibleMorphism.mono_or_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : CategoryTheory.Mono f ∨ CategoryTheory.Epi f

An irreducible morphism in an abelian category is monic or epic.

theorem QuotientSubmoduleEquidistribution.mono_comp_of_weakKernel_component {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z U V : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hweak : ∀ (W : C) (q : W ⟶ Y), CategoryTheory.CategoryStruct.comp q g = 0 → ∃ (l : W ⟶ X), CategoryTheory.CategoryStruct.comp l f = q) {p : Y ⟶ U} (hfp : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f p)) {j : V ⟶ Y} (hj : CategoryTheory.Mono j) (hjp : CategoryTheory.CategoryStruct.comp j p = 0) : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp j g)

A componentwise form of the kernel argument in Ringel's support lemma.

Suppose every morphism killed by g factors through f. If the component f ≫ p is monic, then every monic morphism j into the middle object which is orthogonal to p remains monic after composition with g.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.component {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (t : A.index.obj) : σ.obj (A.label t) ⟶ σ.obj z

The component from one chosen middle summand to the endpoint of a minimal right almost-split map.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.component_irreducible {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (t : A.index.obj) : IsIrreducibleMorphism (component σ A t)

Each displayed component of a minimal right almost-split map is irreducible.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.component_mono_or_epi {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (t : A.index.obj) : CategoryTheory.Mono (component σ A t) ∨ CategoryTheory.Epi (component σ A t)

Every displayed right almost-split component is monic or epic.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.component {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) (t : A.index.obj) : σ.obj z ⟶ σ.obj (A.label t)

The component from the start of a minimal left almost-split map to one chosen middle summand.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.component_irreducible {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) (t : A.index.obj) : IsIrreducibleMorphism (component σ A t)

Each displayed component of a minimal left almost-split map is irreducible.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.component_mono_or_epi {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) (t : A.index.obj) : CategoryTheory.Mono (component σ A t) ∨ CategoryTheory.Epi (component σ A t)

Every displayed left almost-split component is monic or epic.