Kernels of minimal right almost-split epimorphisms

This file proves the kernel half of the abstract Auslander--Reiten sequence theorem needed for mesh rotation. In an abelian category, the kernel inclusion of a right-minimal right almost-split epimorphism is left almost split. For finite-length finitely generated modules its source is indecomposable and noninjective. At a chosen indecomposable endpoint the kernel inclusion is also left minimal.

No presentation or classification of an algebra or of its modules is used.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.kernel_ι_isLeftAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {E Z : C} (f : E ⟶ Z) [CategoryTheory.Epi f] (hf : IsRightAlmostSplit f) (hmin : IsRightMinimal f) : IsLeftAlmostSplit (CategoryTheory.Limits.kernel.ι f)

The kernel inclusion of a right-minimal right almost-split epimorphism is left almost split.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.not_injective_source {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (i : A ⟶ B) [CategoryTheory.Mono i] (hi : IsLeftAlmostSplit i) : ¬CategoryTheory.Injective A

A left almost-split monomorphism cannot start at an injective object.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsLeftAlmostSplit.isIndecomposableModule_source {R : Type uR} [Ring R] {A B : FGModuleCat R} (i : A ⟶ B) (hi : IsLeftAlmostSplit i) : Foundation.IsIndecomposableModule R ↑A

The source of a left almost-split morphism of finitely generated modules is indecomposable.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsRightAlmostSplit.epi_of_not_projective_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {E : FGModuleCat R} {z : ι} (f : E ⟶ σ.obj z) (hf : IsRightAlmostSplit f) (hz : ¬CategoryTheory.Projective (σ.obj z)) : CategoryTheory.Epi f

A right almost-split map to a nonprojective chosen indecomposable is epic.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsRightAlmostSplit.kernel_ι_isLeftMinimal_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {E : FGModuleCat R} {z : ι} (f : E ⟶ σ.obj z) [CategoryTheory.Epi f] (hf : IsRightAlmostSplit f) (hk : IsLeftAlmostSplit (CategoryTheory.Limits.kernel.ι f)) : IsLeftMinimal (CategoryTheory.Limits.kernel.ι f)

Once its kernel inclusion is left almost split, a right almost-split epimorphism to a chosen indecomposable has a left-minimal kernel inclusion.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.kernel_ar_sequence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (hz : ¬CategoryTheory.Projective (σ.obj z)) : IsLeftAlmostSplit (CategoryTheory.Limits.kernel.ι A.map) ∧ IsLeftMinimal (CategoryTheory.Limits.kernel.ι A.map) ∧ Foundation.IsIndecomposableModule R ↑(CategoryTheory.Limits.kernel A.map) ∧ ¬CategoryTheory.Injective (CategoryTheory.Limits.kernel A.map)

The kernel of a chosen minimal right almost-split map at a nonprojective endpoint is the start of a minimal left almost-split map and is an indecomposable noninjective module.