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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.IndecomposableSkeleton.qSet {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) : Set ι

Indecomposable representatives lying in Fac(add S).

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

Indecomposable representatives lying in Sub(add S).

def MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.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 MBDVendor.QSE.IndecomposableSkeleton.qClosure_isFinitary {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.qClosure.IsFinitary

Quotient closure is finitary.

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

Submodule closure is finitary.