Quotient and submodule generation on an indecomposable skeleton

This file defines membership in add S, Fac(add S), and Sub(add S) by explicit finite biproduct presentations. The finite indexing type is bundled so that iterated finite sums can be flattened without any cardinality bookkeeping.

@[reducible, inline]

noncomputable abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sumOver {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (J : FintypeCat) (a : J.obj → ι) : FGModuleCat R

A finite direct sum indexed by a bundled finite type.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AddPresentation {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Type (max (max 1 v) w)

A concrete presentation of X as an object of add S.

• index : FintypeCat
• label : self.index.obj → ι
• mem (t : self.index.obj) : self.label t ∈ S
• iso : X ≅ σ.sumOver self.index self.label

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.FacPresentation {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Type (max (max 1 v) w)

A concrete presentation of X as a quotient of an object of add S.

• index : FintypeCat
• label : self.index.obj → ι
• mem (t : self.index.obj) : self.label t ∈ S
• map : σ.sumOver self.index self.label ⟶ X
• epi : CategoryTheory.Epi self.map

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.SubPresentation {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Type (max (max 1 v) w)

A concrete presentation of X as a submodule of an object of add S.

• index : FintypeCat
• label : self.index.obj → ι
• mem (t : self.index.obj) : self.label t ∈ S
• map : X ⟶ σ.sumOver self.index self.label
• mono : CategoryTheory.Mono self.map

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.InAdd {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Prop

Membership in the additive closure of the selected representatives.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.InFac {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Prop

Membership in the quotient closure Fac(add S).

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.InSub {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Prop

Membership in the submodule closure Sub(add S).

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

Indecomposable representatives lying in Fac(add S).

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

Indecomposable representatives lying in Sub(add S).

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

Enlarging the selected set preserves a quotient presentation.

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

Enlarging the selected set preserves a submodule presentation.

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

Quotient generation is monotone in the selected representatives.

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

Submodule generation is monotone in the selected representatives.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.subset_qSet {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : S ⊆ σ.qSet S

Every selected representative lies in its quotient closure.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.subset_sSet {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : S ⊆ σ.sSet S

Every selected representative lies in its submodule closure.

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

An iterated quotient presentation can be flattened to one finite direct sum.

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

An iterated submodule presentation can be flattened to one finite direct sum.

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

Quotient generation is idempotent.

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

Submodule generation is idempotent.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : SetClosure ι

Quotient closure as a genuine closure operator on the representative type.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosure {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : SetClosure ι

Submodule closure as a genuine closure operator on the representative type.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qSet_finite_witness {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {j : ι} (hj : j ∈ σ.qSet S) : ∃ (T : Set ι), T.Finite ∧ T ⊆ S ∧ j ∈ σ.qSet T

Membership in quotient closure is witnessed by finitely many selected representatives.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sSet_finite_witness {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {j : ι} (hj : j ∈ σ.sSet S) : ∃ (T : Set ι), T.Finite ∧ T ⊆ S ∧ j ∈ σ.sSet T

Membership in submodule closure is witnessed by finitely many selected representatives.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure_isFinitary {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.qClosure.IsFinitary

Quotient closure is finitary.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosure_isFinitary {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.sClosure.IsFinitary

Submodule closure is finitary.