Extremality and relative split injectivity

This file gives the direct submodule-side bridge between extreme points and relative split injectives. The proof uses common kernels and the nilpotent Jacobson radical; it does not invoke categorical duality or Krull--Schmidt multiplicity uniqueness.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsRelativeSplitInjective {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) : Prop

An indecomposable is relatively split injective in C when every monomorphism from it to an explicitly presented object of add C admits a retraction.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.not_splitMono_of_labels_ne {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {x : ι} (P : σ.SubPresentation S (σ.obj x)) (hne : ∀ (t : P.index.obj), x ≠ P.label t) : ¬Nonempty (CategoryTheory.SplitMono P.map)

A split embedding of X into a sum of indecomposables all distinct from X would put the identity in the endomorphism radical.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.splitMono_of_isUnit_component {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {x : ι} (P : σ.SubPresentation S (σ.obj x)) (t : P.index.obj) (ht : P.label t = x) (hunit : IsUnit (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp P.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : P.index.obj) => σ.obj (P.label j)) t) (CategoryTheory.eqToHom ⋯))).hom)) : Nonempty (CategoryTheory.SplitMono P.map)

If a component of a presentation is an invertible endomorphism of the source representative, then the whole presentation map splits.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.splitMono_of_not_mem_sClosure_diff {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) [IsArtinianRing (Module.End R ↑(σ.obj x))] (hnot : x ∉ σ.sClosure (C \ {x})) (P : σ.SubPresentation C (σ.obj x)) : Nonempty (CategoryTheory.SplitMono P.map)

If x is not generated by the other members of C, every monomorphism from obj x to an object of add C splits. Otherwise all components landing in a copy of obj x would be radical, and the common kernel argument would generate x from C \ {x}.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.not_mem_sClosure_diff_of_relativeSplitInjective {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) (hrel : σ.IsRelativeSplitInjective C x) : x ∉ σ.sClosure (C \ {x})

Relative split injectivity prevents x from embedding into a sum of the other members of C.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.not_mem_sClosure_diff_iff_relativeSplitInjective {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) [IsArtinianRing (Module.End R ↑(σ.obj x))] : x ∉ σ.sClosure (C \ {x}) ↔ σ.IsRelativeSplitInjective C x

The split-injective bridge, in a slightly stronger form not requiring C itself to be closed.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.extremal_iff_isRelativeSplitInjective_of_sClosed {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) [IsArtinianRing (Module.End R ↑(σ.obj x))] (_hC : σ.sClosure.IsClosed C) (_hxC : x ∈ C) : x ∉ σ.sClosure (C \ {x}) ↔ σ.IsRelativeSplitInjective C x

For an s-closed set and one of its members, deletion fails to regenerate that member exactly when the member is relatively split injective.