Simple Modules #

Main Definitions #

IsSimpleModule indicates that a module has no proper submodules (the only submodules are ⊥ and ⊤).
IsSemisimpleModule indicates that every submodule has a complement, or equivalently, the module is a direct sum of simple modules.
A DivisionRing structure on the endomorphism ring of a simple module.

Main Results #

Schur's Lemma: bijective_or_eq_zero shows that a linear map between simple modules is either bijective or 0, leading to a DivisionRing structure on the endomorphism ring.
isSimpleModule_iff_quot_maximal: a module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal.
sSup_simples_eq_top_iff_isSemisimpleModule: a module is semisimple iff it is generated by its simple submodules.
IsSemisimpleModule.annihilator_isRadical: the annihilator of a semisimple module over a commutative ring is a radical ideal.
IsSemisimpleModule.submodule, IsSemisimpleModule.quotient: any submodule or quotient module of a semisimple module is semisimple.
isSemisimpleModule_of_isSemisimpleModule_submodule: a module generated by semisimple submodules is itself semisimple.
IsSemisimpleRing.isSemisimpleModule: every module over a semisimple ring is semisimple.
instIsSemisimpleRingForAllRing: a finite product of semisimple rings is semisimple.
RingHom.isSemisimpleRing_of_surjective: any quotient of a semisimple ring is semisimple.

TODO #

Artin-Wedderburn Theory
Unify with the work on Schur's Lemma in a category theory context

source

@[reducible, inline]

abbrev IsSimpleModule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] :

Prop

A module is simple when it has only two submodules, ⊥ and ⊤.

Equations

IsSimpleModule R M = IsSimpleOrder (Submodule R M)

Instances For

source

@[reducible, inline]

abbrev IsSemisimpleModule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] :

Prop

A module is semisimple when every submodule has a complement, or equivalently, the module is a direct sum of simple modules.

Equations

IsSemisimpleModule R M = ComplementedLattice (Submodule R M)

Instances For

source

@[reducible, inline]

abbrev IsSemisimpleRing (R : Type u_2) [Ring R] :

Prop

A ring is semisimple if it is semisimple as a module over itself.

Equations

IsSemisimpleRing R = IsSemisimpleModule R R

Instances For

source

theorem RingEquiv.isSemisimpleRing (R : Type u_2) (S : Type u_3) [Ring R] [Ring S] (e : R ≃+* S) [IsSemisimpleRing R] :

IsSemisimpleRing S

source

theorem IsSimpleModule.nontrivial (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSimpleModule R M] :

Nontrivial M

source

theorem LinearMap.isSimpleModule_iff_of_bijective {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N) (hl : Function.Bijective ⇑l) :

IsSimpleModule R M ↔ IsSimpleModule S N

source

theorem IsSimpleModule.congr {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (l : M ≃ₗ[R] N) [IsSimpleModule R N] :

IsSimpleModule R M

source

theorem isSimpleModule_iff_isAtom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} :

IsSimpleModule R ↥m ↔ IsAtom m

source

theorem isSimpleModule_iff_isCoatom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} :

IsSimpleModule R (M ⧸ m) ↔ IsCoatom m

source

theorem covBy_iff_quot_is_simple {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {A B : Submodule R M} (hAB : A ≤ B) :

A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)

source

@[simp]

theorem IsSimpleModule.isAtom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} [IsSimpleModule R ↥m] :

IsAtom m

source

theorem IsSimpleModule.span_singleton_eq_top (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {m : M} (hm : m ≠ 0) :

Submodule.span R {m} = ⊤

source

instance IsSimpleModule.instIsPrincipal (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] (S : Submodule R M) :

S.IsPrincipal

source

theorem IsSimpleModule.toSpanSingleton_surjective (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {m : M} (hm : m ≠ 0) :

Function.Surjective ⇑(LinearMap.toSpanSingleton R M m)

source

theorem IsSimpleModule.ker_toSpanSingleton_isMaximal (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {m : M} (hm : m ≠ 0) :

Ideal.IsMaximal (LinearMap.ker (LinearMap.toSpanSingleton R M m))

source

instance IsSimpleModule.instIsNoetherian (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] :

IsNoetherian R M

source

theorem isSimpleModule_iff_quot_maximal {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :

IsSimpleModule R M ↔ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal (not necessarily unique if the ring is not commutative).

source

theorem IsSimpleModule.annihilator_isMaximal {M : Type u_4} [AddCommGroup M] {R : Type u_6} [CommRing R] [Module R M] [simple : IsSimpleModule R M] :

(Module.annihilator R M).IsMaximal

In general, the annihilator of a simple module is called a primitive ideal, and it is always a two-sided prime ideal, but mathlib's Ideal.IsPrime is not the correct definition for noncommutative rings.

source

theorem isSimpleModule_iff_toSpanSingleton_surjective {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :

IsSimpleModule R M ↔ Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)

source

theorem isSimpleModule_self_iff_isUnit {R : Type u_2} [Ring R] :

IsSimpleModule R R ↔ Nontrivial R ∧ ∀ (x : R), x ≠ 0 → IsUnit x

A ring is a simple module over itself iff it is a division ring.

source

theorem isSimpleModule_iff_finrank_eq_one {M : Type u_4} [AddCommGroup M] {R : Type u_6} [DivisionRing R] [Module R M] :

IsSimpleModule R M ↔ Module.finrank R M = 1

source

theorem IsSemisimpleModule.of_sSup_simples_eq_top {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (h : sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤) :

IsSemisimpleModule R M

source

@[deprecated IsSemisimpleModule.of_sSup_simples_eq_top]

theorem is_semisimple_of_sSup_simples_eq_top {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (h : sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤) :

IsSemisimpleModule R M

Alias of IsSemisimpleModule.of_sSup_simples_eq_top.

source

theorem IsSemisimpleModule.eq_bot_or_exists_simple_le {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (N : Submodule R M) :

N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m

source

theorem IsSemisimpleModule.sSup_simples_le {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (N : Submodule R M) :

sSup {m : Submodule R M | IsSimpleModule R ↥m ∧ m ≤ N} = N

source

theorem IsSemisimpleModule.exists_simple_submodule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Nontrivial M] :

∃ (m : Submodule R M), IsSimpleModule R ↥m

source

theorem IsSemisimpleModule.sSup_simples_eq_top (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :

sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤

source

theorem IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :

∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

source

@[deprecated IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top]

theorem IsSemisimpleModule.exists_setIndependent_sSup_simples_eq_top (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :

∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Alias of IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top.

source

theorem IsSemisimpleModule.annihilator_isRadical (M : Type u_4) [AddCommGroup M] (R : Type u_6) [CommRing R] [Module R M] [IsSemisimpleModule R M] :

(Module.annihilator R M).IsRadical

The annihilator of a semisimple module over a commutative ring is a radical ideal.

source

instance IsSemisimpleModule.submodule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} :

IsSemisimpleModule R ↥m

source

theorem IsSemisimpleModule.congr {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] (e : N ≃ₗ[R] M) :

IsSemisimpleModule R N

source

instance IsSemisimpleModule.quotient {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} [IsSemisimpleModule R M] :

IsSemisimpleModule R (M ⧸ m)

source

@[instance 100]

instance IsSemisimpleModule.instIsNoetherianOfFinite {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] :

IsNoetherian R M

source

theorem IsSemisimpleModule.range {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] (f : M →ₗ[R] N) :

IsSemisimpleModule R ↥(LinearMap.range f)

source

theorem LinearMap.isSemisimpleModule_iff_of_bijective {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] {M' : Type u_6} [AddCommGroup M'] [Module R M'] {N' : Type u_7} [AddCommGroup N'] [Module S N'] {σ : R →+* S} (l : M' →ₛₗ[σ] N') [RingHomSurjective σ] (hl : Function.Bijective ⇑l) :

IsSemisimpleModule R M' ↔ IsSemisimpleModule S N'

source

theorem sSup_simples_eq_top_iff_isSemisimpleModule {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :

sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤ ↔ IsSemisimpleModule R M

A module is semisimple iff it is generated by its simple submodules.

source

@[deprecated sSup_simples_eq_top_iff_isSemisimpleModule]

theorem is_semisimple_iff_top_eq_sSup_simples {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :

sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤ ↔ IsSemisimpleModule R M

Alias of sSup_simples_eq_top_iff_isSemisimpleModule.

A module is semisimple iff it is generated by its simple submodules.

source

theorem isSemisimpleModule_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {s : Set ι} {p : ι → Submodule R M} (hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)) (hp' : ⨆ i ∈ s, p i = ⊤) :

IsSemisimpleModule R M

A module generated by semisimple submodules is itself semisimple.

source

theorem isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {s : Set ι} {p : ι → Submodule R M} (hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)) :

IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

source

theorem isSemisimpleModule_of_isSemisimpleModule_submodule' {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {p : ι → Submodule R M} (hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)) (hp' : ⨆ (i : ι), p i = ⊤) :

IsSemisimpleModule R M

source

theorem IsSemisimpleModule.sup {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {p q : Submodule R M} :

IsSemisimpleModule R ↥p → IsSemisimpleModule R ↥q → IsSemisimpleModule R ↥(p ⊔ q)

source

instance IsSemisimpleRing.isSemisimpleModule {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] :

IsSemisimpleModule R M

source

instance IsSemisimpleRing.isCoatomic_submodule {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] :

IsCoatomic (Submodule R M)

source

instance instIsSemisimpleRingForallOfFinite {ι : Type u_7} [Finite ι] (R : ι → Type u_6) [(i : ι) → Ring (R i)] [∀ (i : ι), IsSemisimpleRing (R i)] :

IsSemisimpleRing ((i : ι) → R i)

A finite product of semisimple rings is semisimple.

source

instance instIsSemisimpleRingProd {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] :

IsSemisimpleRing (R × S)

A binary product of semisimple rings is semisimple.

source

theorem RingHom.isSemisimpleRing_of_surjective {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) [IsSemisimpleRing R] :

IsSemisimpleRing S

source

theorem IsSemisimpleRing.ideal_eq_span_idempotent {R : Type u_2} [Ring R] [IsSemisimpleRing R] (I : Ideal R) :

∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}

source

instance instIsPrincipalIdealRingOfIsSemisimpleRing {R : Type u_2} [Ring R] [IsSemisimpleRing R] :

IsPrincipalIdealRing R

source

theorem LinearMap.injective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] (f : M →ₗ[R] N) :

Function.Injective ⇑f ∨ f = 0

source

theorem LinearMap.injective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] {f : M →ₗ[R] N} (h : f ≠ 0) :

Function.Injective ⇑f

source

theorem LinearMap.surjective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] (f : M →ₗ[R] N) :

Function.Surjective ⇑f ∨ f = 0

source

theorem LinearMap.surjective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :

Function.Surjective ⇑f

source

theorem LinearMap.bijective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) :

Function.Bijective ⇑f ∨ f = 0

Schur's Lemma for linear maps between (possibly distinct) simple modules

source

theorem LinearMap.bijective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :

Function.Bijective ⇑f

source

theorem LinearMap.isCoatom_ker_of_surjective {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f) :

IsCoatom (LinearMap.ker f)

source

noncomputable instance Module.End.divisionRing {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [DecidableEq (Module.End R M)] [IsSimpleModule R M] :

DivisionRing (Module.End R M)

Schur's Lemma makes the endomorphism ring of a simple module a division ring.

Equations

Module.End.divisionRing = DivisionRing.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

source

def JordanHolderModule.Iso {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (X Y : Submodule R M × Submodule R M) :

Prop

An isomorphism X₂ / X₁ ∩ X₂ ≅ Y₂ / Y₁ ∩ Y₂ of modules for pairs (X₁,X₂) (Y₁,Y₂) : Submodule R M

Equations

JordanHolderModule.Iso X Y = Nonempty ((↥X.2 ⧸ Submodule.comap X.2.subtype X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap Y.2.subtype Y.1)

Instances For

source

theorem JordanHolderModule.iso_symm {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {X Y : Submodule R M × Submodule R M} :

JordanHolderModule.Iso X Y → JordanHolderModule.Iso Y X

source

theorem JordanHolderModule.iso_trans {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {X Y Z : Submodule R M × Submodule R M} :

JordanHolderModule.Iso X Y → JordanHolderModule.Iso Y Z → JordanHolderModule.Iso X Z

source

theorem JordanHolderModule.second_iso {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {X Y : Submodule R M} :

X ⋖ X ⊔ Y → JordanHolderModule.Iso (X, X ⊔ Y) (X ⊓ Y, Y)

source

instance JordanHolderModule.instJordanHolderLattice {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :

JordanHolderLattice (Submodule R M)

Equations

One or more equations did not get rendered due to their size.

Documentation

Mathlib.RingTheory.SimpleModule

Simple Modules #

Main Definitions #

Main Results #

TODO #