Anti-exchange for quotient closure

This file formalizes the trace-and-radical proof of anti-exchange from the manuscript. The proof works on a chosen indecomposable skeleton and assumes that each indecomposable endomorphism ring is Artinian. That is the exact ring-theoretic input used to make its Jacobson radical nilpotent.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.pointTrace {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (i : ι) (X : FGModuleCat R) : Submodule R ↑X

The sum of the ranges of all maps from one indecomposable representative.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.trace_singleton_eq_pointTrace {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (i : ι) (X : FGModuleCat R) : σ.trace {i} X = σ.pointTrace i X

A singleton trace is already generated by maps from the single indecomposable, rather than requiring maps from arbitrary finite sums of its copies.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.trace_fullyInvariant_linear {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} (X : FGModuleCat R) (f : Module.End R ↑X) : Submodule.map f (σ.trace S X) ≤ σ.trace S X

The selected trace is fully invariant under every underlying endomorphism, not just an endomorphism already presented categorically.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.map_pointTrace_le {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {i : ι} {X Y : FGModuleCat R} (f : X ⟶ Y) : Submodule.map (ModuleCat.Hom.hom f.hom) (σ.pointTrace i X) ≤ σ.pointTrace i Y

Postcomposition sends the point trace of i into the point trace of i.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.comp_mem_end_jacobson {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {x y : ι} (hxy : x ≠ y) (f : σ.obj y ⟶ σ.obj x) (g : σ.obj x ⟶ σ.obj y) : ModuleCat.Hom.hom f.hom ∘ₗ ModuleCat.Hom.hom g.hom ∈ Ring.jacobson (Module.End R ↑(σ.obj x))

If x and y index nonisomorphic representatives, every endomorphism of X factoring through Y belongs to the Jacobson radical of End(X).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.pointTrace_le_trace_sup_jacobson {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) {x y : ι} (hxy : x ≠ y) (hY : σ.trace C (σ.obj y) ⊔ σ.pointTrace x (σ.obj y) = ⊤) : σ.pointTrace y (σ.obj x) ≤ σ.trace C (σ.obj x) ⊔ idealRange (Ring.jacobson (Module.End R ↑(σ.obj x)))

Substituting generation of Y by C and X into all maps Y → X shows that the point trace of Y in X is generated by the trace of C and the Jacobson radical of End(X).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure_isAntiExchange {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) [∀ (i : ι), IsArtinianRing (Module.End R ↑(σ.obj i))] : σ.qClosure.IsAntiExchange

Quotient closure satisfies anti-exchange whenever the relevant endomorphism rings are Artinian.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure_isConvexGeometry {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) [∀ (i : ι), IsArtinianRing (Module.End R ↑(σ.obj i))] : σ.qClosure.IsConvexGeometry

Under the Artinian endomorphism-ring hypothesis, quotient closure is a convex geometry.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure_isAntiExchange_of_finiteDimensional {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {K : Type u_1} [Field K] [Algebra K R] [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] : σ.qClosure.IsAntiExchange

The manuscript's finite-dimensional-over-a-field hypothesis supplies the Artinian endomorphism rings required for quotient anti-exchange.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosure_isConvexGeometry_of_finiteDimensional {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {K : Type u_1} [Field K] [Algebra K R] [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] : σ.qClosure.IsConvexGeometry

Quotient closure is a convex geometry for the finite-dimensional module setup used in the manuscript.