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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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.