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

@[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)

@[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)

@[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

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

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

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

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

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

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

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)

@[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

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} = ⊤

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

Equations

• ⋯ = ⋯

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)

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))

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

Equations

• ⋯ = ⋯

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

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.

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)

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.

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

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

@[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.

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

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

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

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} = ⊤

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

@[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.

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.

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

Equations

• ⋯ = ⋯

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

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)

Equations

• ⋯ = ⋯

@[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

Equations

• ⋯ = ⋯

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)

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'

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.

@[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.

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.

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)

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

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)

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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

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}

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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)

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) ⋯

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)

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

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

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)

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.