Extremality and relative split projectivity

For an indecomposable representative x, failure of x to be generated by C \ {x} is equivalent to every epimorphism from an explicitly presented object of add C to x splitting.

The difficult implication uses nilpotence of the Jacobson radical of End(x). In the current skeleton this is supplied by the same Artinian endomorphism-ring hypothesis used for anti-exchange.

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

Relative split projectivity with respect to add C, expressed on the explicit finite-sum skeleton: every epimorphic presentation from add C admits a section.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation.component {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (P : σ.FacPresentation S X) (t : P.index.obj) : σ.obj (P.label t) ⟶ X

The map from one summand of a quotient presentation to its target.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation.map_apply_eq_sum_components {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (P : σ.FacPresentation S X) [Fintype P.index.obj] (z : ↑(σ.sumOver P.index P.label)) : (ModuleCat.Hom.hom P.map.hom) z = ∑ t : P.index.obj, (ModuleCat.Hom.hom (component σ P t).hom) ((ModuleCat.Hom.hom (CategoryTheory.Limits.biproduct.π (fun (t : P.index.obj) => σ.obj (P.label t)) t).hom) z)

A quotient presentation is pointwise the sum of its component maps.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation.isSplitEpi_of_isUnit_component {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {x : ι} (P : σ.FacPresentation S (σ.obj x)) (t : P.index.obj) (ht : P.label t = x) (hunit : IsUnit (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (component σ P t)).hom)) : CategoryTheory.IsSplitEpi P.map

If one component, transported to an endomorphism of the target representative, is a unit, the whole presentation splits.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation.not_isUnit_component_of_not_isSplitEpi {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {x : ι} (P : σ.FacPresentation S (σ.obj x)) (hP : ¬CategoryTheory.IsSplitEpi P.map) (t : P.index.obj) (ht : P.label t = x) : ¬IsUnit (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (component σ P t)).hom)

If a presentation does not split, every component labelled by the target representative becomes a nonunit endomorphism after transport.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation.range_le_trace_sdiff_sup_idealRange {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {C : Set ι} {x : ι} (P : σ.FacPresentation C (σ.obj x)) (hP : ¬CategoryTheory.IsSplitEpi P.map) : (ModuleCat.Hom.hom P.map.hom).range ≤ σ.trace (C \ {x}) (σ.obj x) ⊔ idealRange (Ring.jacobson (Module.End R ↑(σ.obj x)))

A nonsplit quotient presentation from add C has range contained in the trace of C \ {x} plus the ranges of radical endomorphisms of x.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isRelativeSplitProjective_of_not_mem_qClosure_sdiff {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) [IsArtinianRing (Module.End R ↑(σ.obj x))] (hx : x ∉ σ.qClosure (C \ {x})) : σ.IsRelativeSplitProjective C x

Extremality implies relative split projectivity. Nilpotence of the Jacobson radical (here obtained from Artinianness of the endomorphism ring) is the extra input needed to discard nonsplit copies of x in a source.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.not_mem_qClosure_sdiff_of_isRelativeSplitProjective {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) (x : ι) (hproj : σ.IsRelativeSplitProjective C x) : x ∉ σ.qClosure (C \ {x})

Relative split projectivity prevents generation by the other selected representatives. This direction only uses locality of End(x), which comes from indecomposability and finite length.

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

The module-theoretic extremality equivalence. It holds for an arbitrary selected set C; only Artinianness of End(x) is used in the difficult implication.

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

The manuscript-context wrapper: C is quotient-closed and contains x. The stronger theorem above shows that these two assumptions locate the statement inside the closed set but are not needed by the equivalence.