Additive subcategories and indecomposable support

The adapter needed by the paper: a full, replete subcategory of finitely generated modules which is closed under finite direct sums and direct summands is completely determined by its indecomposable support.

No Krull--Schmidt multiplicity-uniqueness theorem is used. The only uniqueness input is the existing radical argument IndecomposableSkeleton.not_splitMono_of_labels_ne.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory {R : Type u} [Ring R] : Type (max u (w + 1))

A literal full additive, replete, summand-closed subcategory, represented by its object predicate. Fullness is supplied by carrier.FullSubcategory; finite-biproduct closure includes the empty biproduct, and retract closure implies repleteness.

• carrier : CategoryTheory.ObjectProperty (FGModuleCat R)
• biproduct_mem (J : FintypeCat) (F : J.obj → FGModuleCat R) : (∀ (j : J.obj), self.carrier (F j)) → self.carrier (⨁ F)
• retract_mem {X Y : FGModuleCat R} : ∀ (a : CategoryTheory.Retract X Y), self.carrier Y → self.carrier X

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.FullSubcategory {R : Type u} [Ring R] (C : AdditiveRepleteSummandSubcategory) : Type (max u (u_1 + 1))

The corresponding literal full subcategory.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.iso_mem {R : Type u} [Ring R] (C : AdditiveRepleteSummandSubcategory) {X Y : FGModuleCat R} (e : X ≅ Y) (hX : C.carrier X) : C.carrier Y

Retract closure entails closure under isomorphisms.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.ext {R : Type u} [Ring R] {C D : AdditiveRepleteSummandSubcategory} (h : ∀ (X : FGModuleCat R), C.carrier X ↔ D.carrier X) : C = D

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.ext_iff {R : Type u} [Ring R] {C D : AdditiveRepleteSummandSubcategory} : C = D ↔ ∀ (X : FGModuleCat R), C.carrier X ↔ D.carrier X

@[instance_reducible]

instance QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.instLE {R : Type u} [Ring R] : LE AdditiveRepleteSummandSubcategory

@[instance_reducible]

instance QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AdditiveRepleteSummandSubcategory.instPartialOrder {R : Type u} [Ring R] : PartialOrder AdditiveRepleteSummandSubcategory

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AddPresentation.of_subset {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S T : Set ι} {X : FGModuleCat R} (P : σ.AddPresentation S X) (hST : S ⊆ T) : σ.AddPresentation T X

Enlarging the support preserves an additive presentation.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_mono {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S T : Set ι} (hST : S ⊆ T) {X : FGModuleCat R} : σ.InAdd S X → σ.InAdd T X

Additive closure is monotone in the support.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_iff_of_iso {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X Y : FGModuleCat R} (e : X ≅ Y) : σ.InAdd S X ↔ σ.InAdd S Y

InAdd is replete.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_biproduct {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} (J : FintypeCat) (F : J.obj → FGModuleCat R) (hF : ∀ (j : J.obj), σ.InAdd S (F j)) : σ.InAdd S (⨁ F)

A finite biproduct of objects in InAdd S again lies in InAdd S.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_obj {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {i : ι} (hi : i ∈ S) : σ.InAdd S (σ.obj i)

Every selected representative belongs to its additive closure.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.index_mem_of_retract_inAdd {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {i : ι} {Y : FGModuleCat R} (r : CategoryTheory.Retract (σ.obj i) Y) (hY : σ.InAdd S Y) : i ∈ S

If an indecomposable representative is a retract of an object in add S, its index already lies in S.

This is the precise substitute for a global Krull--Schmidt uniqueness API: otherwise the split embedding into the displayed sum would have all its components in the endomorphism radical.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_of_retract {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X Y : FGModuleCat R} (r : CategoryTheory.Retract X Y) (hY : σ.InAdd S Y) : σ.InAdd S X

InAdd S is closed under retracts (direct summands).

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.generated {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : AdditiveRepleteSummandSubcategory

The literal additive/replete/summand-closed subcategory generated by a set of indecomposable representatives.

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

The indecomposable support of a literal additive subcategory.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.support_generated {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : σ.support (σ.generated S) = S

Generating and then taking support returns the original set.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.generated_support {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : AdditiveRepleteSummandSubcategory) : σ.generated (σ.support C) = C

Taking support and then additive closure returns the original literal subcategory.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.generated_monotone {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : Monotone σ.generated

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.support_monotone {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : Monotone σ.support

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.supportOrderIso {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : AdditiveRepleteSummandSubcategory ≃o Set ι

Order equivalence between indecomposable supports and literal full additive, replete, summand-closed subcategories.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_qSet_of_inFac {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (hX : σ.InFac S X) : σ.InAdd (σ.qSet S) X

Every object presented as a quotient of add S belongs to add (qSet S).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.inAdd_sSet_of_inSub {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (hX : σ.InSub S X) : σ.InAdd (σ.sSet S) X

Every object presented as a subobject of add S belongs to add (sSet S).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosed_iff_generated_isClosedUnderQuotients {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : σ.qClosure.IsClosed S ↔ (σ.generated S).carrier.IsClosedUnderQuotients

q-closed supports are exactly the supports whose literal additive subcategory is closed under categorical quotients.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosed_iff_generated_isClosedUnderSubobjects {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : σ.sClosure.IsClosed S ↔ (σ.generated S).carrier.IsClosedUnderSubobjects

s-closed supports are exactly the supports whose literal additive subcategory is closed under categorical subobjects.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.QuotientClosedAdditiveSubcategory {R : Type u} [Ring R] : Type (max 0 u (u_1 + 1))

Literal additive subcategories which are also quotient-closed.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.SubobjectClosedAdditiveSubcategory {R : Type u} [Ring R] : Type (max 0 u (u_1 + 1))

Literal additive subcategories which are also subobject-closed.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.quotientClosedSupportOrderIso {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : QuotientClosedAdditiveSubcategory ≃o ClosureOperator.Closeds σ.qClosure

The exact order-level adapter for the paper's quotient-closed subcategories.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.subobjectClosedSupportOrderIso {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : SubobjectClosedAdditiveSubcategory ≃o ClosureOperator.Closeds σ.sClosure

The exact order-level adapter for the paper's subobject-closed subcategories.