Anti-exchange for submodule closure

This file gives the direct reject-and-kernel dual of the trace proof in AntiExchange. In particular it does not assume an unformalized duality equivalence: the common kernels of maps through a distinct indecomposable are iterated through the nilpotent Jacobson radical.

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

The intersection of the kernels of all maps to one indecomposable representative.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_le_ker_of_mem {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {S : Set ι} {i : ι} (hi : i ∈ S) {X : FGModuleCat R} (f : X ⟶ σ.obj i) : σ.reject S X ≤ (ModuleCat.Hom.hom f.hom).ker

Every map to a selected indecomposable occurs in the reject intersection.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_singleton_eq_pointReject {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (i : ι) (X : FGModuleCat R) : σ.reject {i} X = σ.pointReject i X

The reject against a singleton is the common kernel of all maps to that indecomposable.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_union {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S T : Set ι) (X : FGModuleCat R) : σ.reject (S ∪ T) X = σ.reject S X ⊓ σ.reject T X

Reject converts unions of selected indecomposables to meets.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_insert {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (S : Set ι) (i : ι) (X : FGModuleCat R) : σ.reject (insert i S) X = σ.reject S X ⊓ σ.pointReject i X

Adjoining one indecomposable intersects with its point reject.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_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 (σ.reject S X) ≤ σ.reject S X

The reject is invariant under every underlying endomorphism.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.reject_inf_idealKernel_eq_bot {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (C : Set ι) {x y : ι} (hxy : x ≠ y) (hX : σ.reject C (σ.obj x) ⊓ σ.pointReject y (σ.obj x) = ⊥) (hY : σ.reject C (σ.obj y) ⊓ σ.pointReject x (σ.obj y) = ⊥) : σ.reject C (σ.obj x) ⊓ idealKernel (Ring.jacobson (Module.End R ↑(σ.obj x))) = ⊥

Mutual one-point submodule generation forces the reject of C in X to meet the common Jacobson-radical kernel trivially.

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

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

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

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

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosure_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)] : σ.sClosure.IsAntiExchange

The manuscript's finite-dimensional-over-a-field hypothesis supplies submodule anti-exchange.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosure_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)] : σ.sClosure.IsConvexGeometry

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

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.quotientSubmodule_finitary_antiExchange_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.IsFinitary ∧ σ.qClosure.IsAntiExchange) ∧ σ.sClosure.IsFinitary ∧ σ.sClosure.IsAntiExchange

The exact combined content of the manuscript's anti-exchange proposition: both closures are finitary and satisfy anti-exchange.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.twoConvexGeometries_of_finiteDimensional {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) [Finite ι] {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 ∧ σ.sClosure.IsConvexGeometry

In finite representation type, quotient and submodule closure give the two finite convex geometries asserted in the manuscript.