The radical of an indecomposable endomorphism ring

The anti-exchange argument uses the Jacobson radical of the local endomorphism ring of an indecomposable finite-length module. Mathlib proves that the Jacobson radical of an Artinian ring is nilpotent. This file identifies its elements with the noninvertible endomorphisms and packages the iteration-on-images argument needed by the manuscript.

theorem QuotientSubmoduleEquidistribution.nonempty_linearEquiv_of_isUnit_comp {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] {Y : Type u_1} [AddCommGroup Y] [Module A Y] (hX : Foundation.IsIndecomposableModule A X) (hY : Foundation.IsIndecomposableModule A Y) (f : Y →ₗ[A] X) (g : X →ₗ[A] Y) (hunit : IsUnit (f ∘ₗ g)) : Nonempty (X ≃ₗ[A] Y)

If a composite X → Y → X is invertible and both modules are indecomposable, then the first map is a linear equivalence onto Y.

theorem QuotientSubmoduleEquidistribution.isUnit_right_of_isUnit_comp {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hXlen : IsFiniteLength A X) (f g : Module.End A X) (hunit : IsUnit (f ∘ₗ g)) : IsUnit g

In a finite-length module, a right factor of an invertible composite endomorphism is invertible.

def QuotientSubmoduleEquidistribution.endNonunitsIdeal {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hX : Foundation.IsIndecomposableModule A X) (hXlen : IsFiniteLength A X) : Ideal (Module.End A X)

For a finite-length indecomposable, the nonunits in its endomorphism ring form its unique maximal left ideal.

@[simp]

theorem QuotientSubmoduleEquidistribution.mem_endNonunitsIdeal_iff {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hX : Foundation.IsIndecomposableModule A X) (hXlen : IsFiniteLength A X) (f : Module.End A X) : f ∈ endNonunitsIdeal hX hXlen ↔ ¬IsUnit f

theorem QuotientSubmoduleEquidistribution.endNonunitsIdeal_isMaximal {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hX : Foundation.IsIndecomposableModule A X) (hXlen : IsFiniteLength A X) : (endNonunitsIdeal hX hXlen).IsMaximal

The ideal of noninvertible endomorphisms is maximal.

theorem QuotientSubmoduleEquidistribution.end_jacobson_eq_nonunits {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hX : Foundation.IsIndecomposableModule A X) (hXlen : IsFiniteLength A X) : Ring.jacobson (Module.End A X) = endNonunitsIdeal hX hXlen

The Jacobson radical of the endomorphism ring is exactly its ideal of noninvertible endomorphisms.

theorem QuotientSubmoduleEquidistribution.mem_end_jacobson_iff_not_isUnit {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (hX : Foundation.IsIndecomposableModule A X) (hXlen : IsFiniteLength A X) (f : Module.End A X) : f ∈ Ring.jacobson (Module.End A X) ↔ ¬IsUnit f

An endomorphism of an indecomposable finite-length module belongs to the Jacobson radical exactly when it is not invertible.

theorem QuotientSubmoduleEquidistribution.isArtinianRing_moduleEnd_of_finiteDimensional {K : Type u_1} {B : Type u_2} {M : Type u_3} [Field K] [Ring B] [Algebra K B] [AddCommGroup M] [Module K M] [Module B M] [IsScalarTower K B M] [FiniteDimensional K M] : IsArtinianRing (Module.End B M)

The endomorphism ring of a module finite-dimensional over a central ground field is Artinian.

def QuotientSubmoduleEquidistribution.idealRange {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (I : Ideal (Module.End A X)) : Submodule A X

The sum of the images of all endomorphisms in a left ideal.

theorem QuotientSubmoduleEquidistribution.range_le_idealRange {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] {I : Ideal (Module.End A X)} (f : Module.End A X) (hf : f ∈ I) : LinearMap.range f ≤ idealRange I

Each ideal element's range belongs to the total ideal range.

@[simp]

theorem QuotientSubmoduleEquidistribution.idealRange_bot {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] : idealRange ⊥ = ⊥

@[simp]

theorem QuotientSubmoduleEquidistribution.idealRange_top {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] : idealRange ⊤ = ⊤

theorem QuotientSubmoduleEquidistribution.map_idealRange_le {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] {I J : Ideal (Module.End A X)} (f : Module.End A X) (hf : f ∈ I) : Submodule.map f (idealRange J) ≤ idealRange (I * J)

Acting by an element of I sends the range of J into the range of the product ideal I * J.

theorem QuotientSubmoduleEquidistribution.eq_top_of_nilpotent_idealRange {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (I : Ideal (Module.End A X)) [I.IsTwoSided] (T : Submodule A X) (hT : ∀ (f : Module.End A X), Submodule.map f T ≤ T) (hI : IsNilpotent I) (hsup : T ⊔ idealRange I = ⊤) : T = ⊤

Nilpotence of an ideal, together with a fully invariant submodule and generation modulo that submodule by the ideal's images, forces the submodule to be the whole module.

def QuotientSubmoduleEquidistribution.idealKernel {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (I : Ideal (Module.End A X)) : Submodule A X

The common kernel of all endomorphisms in a left ideal.

theorem QuotientSubmoduleEquidistribution.idealKernel_le_ker {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] {I : Ideal (Module.End A X)} (f : Module.End A X) (hf : f ∈ I) : idealKernel I ≤ LinearMap.ker f

The common ideal kernel lies in the kernel of each ideal element.

@[simp]

theorem QuotientSubmoduleEquidistribution.idealKernel_bot {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] : idealKernel ⊥ = ⊤

@[simp]

theorem QuotientSubmoduleEquidistribution.idealKernel_top {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] : idealKernel ⊤ = ⊥

theorem QuotientSubmoduleEquidistribution.eq_bot_of_inf_idealKernel {A : Type u} {X : Type v} [Ring A] [AddCommGroup X] [Module A X] (I : Ideal (Module.End A X)) [I.IsTwoSided] (K : Submodule A X) (hK : ∀ (f : Module.End A X), Submodule.map f K ≤ K) (hI : IsNilpotent I) (hinf : K ⊓ idealKernel I = ⊥) : K = ⊥

If a fully invariant submodule meets the common kernel of a nilpotent ideal trivially, then the submodule itself is trivial.