Trace and reject submodules

The quotient-side anti-exchange proof is organized around the trace of add S in a target module. We represent a map from add S by an explicit finite direct-sum presentation. This convention makes the equivalence between trace generation and Fac(add S) literal rather than implicit.

The dual object is the intersection of the kernels of all maps into explicit finite sums from add S.

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

A map to X from one explicitly presented 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

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

A map from X to one explicitly presented 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

noncomputable def MBDVendor.QSE.IndecomposableSkeleton.trace {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Submodule R ↑X

The trace of add S in X: the sum of the ranges of all maps from explicit finite sums of selected representatives.

noncomputable def MBDVendor.QSE.IndecomposableSkeleton.reject {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : Submodule R ↑X

The reject of add S in X: the intersection of the kernels of all maps to explicit finite sums of selected representatives.

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_eq_bot_of_forall_hom_eq_zero {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (hzero : ∀ i ∈ S, ∀ (f : σ.obj i ⟶ X), f = 0) : σ.trace S X = ⊥

If all maps from selected representatives to X vanish, their trace in X is zero.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_eq_top_of_forall_hom_eq_zero {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (hzero : ∀ i ∈ S, ∀ (f : X ⟶ σ.obj i), f = 0) : σ.reject S X = ⊤

Dually, if all maps from X to selected representatives vanish, their reject in X is all of X.

theorem MBDVendor.QSE.IndecomposableSkeleton.range_le_trace {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (f : σ.SelectedMapTo S X) : (ModuleCat.Hom.hom f.map.hom).range ≤ σ.trace S X

The range of every selected map lies in the trace.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_le_ker {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (f : σ.SelectedMapFrom S X) : σ.reject S X ≤ (ModuleCat.Hom.hom f.map.hom).ker

The reject lies in the kernel of every selected map.

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_mono {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S T : Set ι} (hST : S ⊆ T) (X : FGModuleCat R) : σ.trace S X ≤ σ.trace T X

Trace is monotone in the selected representatives.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_anti {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S T : Set ι} (hST : S ⊆ T) (X : FGModuleCat R) : σ.reject T X ≤ σ.reject S X

Reject is antitone in the selected representatives.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_empty {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (X : FGModuleCat R) : σ.trace ∅ X = ⊥

The trace of the empty selection is zero. A selected map with no labels has an empty biproduct as its source and is therefore the zero map.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_empty {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (X : FGModuleCat R) : σ.reject ∅ X = ⊤

The reject of the empty selection is the whole module. Every map to an empty biproduct is zero.

theorem MBDVendor.QSE.IndecomposableSkeleton.inFac_iff_trace_eq_top {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) : σ.InFac S X ↔ σ.trace S X = ⊤

Quotient generation is equivalent to the trace filling the target module.

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_qSet_iff_trace_eq_top {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.qSet S ↔ σ.trace S (σ.obj j) = ⊤

Membership in quotient closure is the trace criterion used throughout the manuscript.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.qSet_empty {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.qSet ∅ = ∅

No nonzero indecomposable is generated by the empty selection.

theorem MBDVendor.QSE.IndecomposableSkeleton.qClosure_isClosed_empty {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.qClosure.IsClosed ∅

The empty set is closed for quotient generation.

theorem MBDVendor.QSE.IndecomposableSkeleton.fg_epi_iff_surjective {R₀ : Type u₀} [Ring R₀] {X Y : FGModuleCat R₀} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(ModuleCat.Hom.hom f.hom)

In FGModuleCat, categorical epimorphisms are exactly surjective underlying linear maps.

theorem MBDVendor.QSE.IndecomposableSkeleton.range_eq_top_of_epi {R₀ : Type u₀} [Ring R₀] {X Y : FGModuleCat R₀} (f : X ⟶ Y) [CategoryTheory.Epi f] : (ModuleCat.Hom.hom f.hom).range = ⊤

An epi in FGModuleCat has full linear range.

theorem MBDVendor.QSE.IndecomposableSkeleton.fg_mono_iff_injective {R : Type u} [Ring R] [IsNoetherianRing R] {X Y : FGModuleCat R} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑(ModuleCat.Hom.hom f.hom)

In FGModuleCat over a noetherian ring, categorical monomorphisms are exactly injective underlying linear maps.

theorem MBDVendor.QSE.IndecomposableSkeleton.ker_eq_bot_of_mono {R : Type u} [Ring R] [IsNoetherianRing R] {X Y : FGModuleCat R} (f : X ⟶ Y) [CategoryTheory.Mono f] : (ModuleCat.Hom.hom f.hom).ker = ⊥

A mono in FGModuleCat over a noetherian ring has zero linear kernel.

noncomputable def MBDVendor.QSE.IndecomposableSkeleton.SelectedMapFrom.flattenFinset {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (F : Finset (σ.SelectedMapFrom S X)) : σ.SelectedMapFrom S X

Flatten a finite family of maps from X into objects of add S to one map from X into a single explicitly presented object of add S.

theorem MBDVendor.QSE.IndecomposableSkeleton.SelectedMapFrom.ker_flattenFinset_le {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X : FGModuleCat R} (F : Finset (σ.SelectedMapFrom S X)) (f : σ.SelectedMapFrom S X) (hf : f ∈ F) : (ModuleCat.Hom.hom (flattenFinset σ F).map.hom).ker ≤ (ModuleCat.Hom.hom f.map.hom).ker

The kernel of the flattened map is contained in the kernel of each map in the finite family.

theorem MBDVendor.QSE.IndecomposableSkeleton.exists_finset_reject_eq {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) (hX : IsFiniteLength R ↑X) : ∃ (F : Finset (σ.SelectedMapFrom S X)), ⨅ f ∈ F, (ModuleCat.Hom.hom f.map.hom).ker = σ.reject S X

In an Artinian module, the intersection defining reject is already the intersection of finitely many selected-map kernels.

theorem MBDVendor.QSE.IndecomposableSkeleton.inSub_of_reject_eq_bot {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) (hX : IsFiniteLength R ↑X) (hreject : σ.reject S X = ⊥) : σ.InSub S X

Vanishing reject gives an embedding into one selected finite sum.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_eq_bot_of_inSub {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) (hsub : σ.InSub S X) : σ.reject S X = ⊥

A submodule presentation is itself one of the maps occurring in the reject intersection, so its monicity forces reject to vanish.

theorem MBDVendor.QSE.IndecomposableSkeleton.inSub_iff_reject_eq_bot {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (X : FGModuleCat R) (hX : IsFiniteLength R ↑X) : σ.InSub S X ↔ σ.reject S X = ⊥

For finite-length modules, submodule generation is exactly reject vanishing.

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_sSet_iff_reject_eq_bot {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.sSet S ↔ σ.reject S (σ.obj j) = ⊥

Membership in submodule closure is the reject criterion.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.sSet_empty {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : σ.sSet ∅ = ∅

No nonzero indecomposable embeds into the empty selected sum.

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

The empty set is closed for submodule generation.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_qClosure_iff_inFac {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.qClosure S ↔ σ.InFac S (σ.obj j)

Membership in the quotient closure, unfolded to its presentation.

@[simp]

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_sClosure_iff_inSub {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.sClosure S ↔ σ.InSub S (σ.obj j)

Membership in the submodule closure, unfolded to its presentation.

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_qClosure_iff_trace_eq_top {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.qClosure S ↔ σ.trace S (σ.obj j) = ⊤

Membership in the quotient closure, expressed by the trace criterion.

theorem MBDVendor.QSE.IndecomposableSkeleton.mem_sClosure_iff_reject_eq_bot {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (j : ι) : j ∈ σ.sClosure S ↔ σ.reject S (σ.obj j) = ⊥

Membership in the submodule closure, expressed by the reject criterion.

theorem MBDVendor.QSE.IndecomposableSkeleton.map_trace_le_trace {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X Y : FGModuleCat R} (f : X ⟶ Y) : Submodule.map (ModuleCat.Hom.hom f.hom) (σ.trace S X) ≤ σ.trace S Y

Postcomposition carries the selected trace into the selected trace. This is the fully invariant property used in the anti-exchange proof.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_le_comap_reject {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {X Y : FGModuleCat R} (f : X ⟶ Y) : σ.reject S X ≤ Submodule.comap (ModuleCat.Hom.hom f.hom) (σ.reject S Y)

Precomposition carries the reject into the inverse image of the reject.

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_fullyInvariant {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} (X : FGModuleCat R) (f : X ⟶ X) : Submodule.map (ModuleCat.Hom.hom f.hom) (σ.trace S X) ≤ σ.trace S X

The trace is stable under every endomorphism of its target.

theorem MBDVendor.QSE.IndecomposableSkeleton.reject_fullyInvariant {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} (X : FGModuleCat R) (f : X ⟶ X) : σ.reject S X ≤ Submodule.comap (ModuleCat.Hom.hom f.hom) (σ.reject S X)

The reject is stable under inverse image by every endomorphism of its source.

theorem MBDVendor.QSE.IndecomposableSkeleton.range_le_trace_of_mem {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {i : ι} (hi : i ∈ S) {X : FGModuleCat R} (f : σ.obj i ⟶ X) : (ModuleCat.Hom.hom f.hom).range ≤ σ.trace S X

A map from one selected indecomposable has range in the trace.

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_union {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S T : Set ι) (X : FGModuleCat R) : σ.trace (S ∪ T) X = σ.trace S X ⊔ σ.trace T X

Trace converts unions of selected indecomposables to joins of submodules.

theorem MBDVendor.QSE.IndecomposableSkeleton.trace_insert {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (i : ι) (X : FGModuleCat R) : σ.trace (insert i S) X = σ.trace S X ⊔ σ.trace {i} X

Adjoining one indecomposable adds precisely its singleton trace.