Simple Modules #
Main Definitions #
IsSimpleModuleindicates that a module has no proper submodules (the only submodules are⊥and⊤).IsSemisimpleModuleindicates that every submodule has a complement, or equivalently, the module is a direct sum of simple modules.- A
DivisionRingstructure on the endomorphism ring of a simple module.
Main Results #
- Schur's Lemma:
bijective_or_eq_zeroshows that a linear map between simple modules is either bijective or 0, leading to aDivisionRingstructure 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]
A module is simple when it has only two submodules, ⊥ and ⊤.
Equations
- IsSimpleModule R M = IsSimpleOrder (Submodule R M)
@[reducible, inline]
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]
A ring is semisimple if it is semisimple as a module over itself.
Equations
theorem
RingEquiv.isSemisimpleRing
(R : Type u_2)
(S : Type u_3)
[Ring R]
[Ring S]
(e : R ≃+* S)
[IsSemisimpleRing R]
:
theorem
IsSimpleModule.nontrivial
(R : Type u_2)
[Ring R]
(M : Type u_4)
[AddCommGroup M]
[Module R M]
[IsSimpleModule R 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)
:
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}
:
theorem
isSimpleModule_iff_isCoatom
{R : Type u_2}
[Ring R]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
{m : Submodule R 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)
:
@[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)
:
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)
:
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)
:
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)
:
instance
IsSimpleModule.instIsNoetherian
(R : Type u_2)
[Ring R]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
[IsSimpleModule R M]
:
IsNoetherian R M
theorem
isSimpleModule_iff_quot_maximal
{R : Type u_2}
[Ring R]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
:
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)
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]
:
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} = ⊤)
:
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)
:
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)
:
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]
:
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]
:
@[deprecated IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top (since := "2024-11-24")]
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]
:
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
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)
:
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)
@[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
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)
:
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)
:
theorem
sSup_simples_eq_top_iff_isSemisimpleModule
{R : Type u_2}
[Ring R]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
:
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 = ⊤)
:
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 = ⊤)
:
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]
:
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)
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.
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.
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]
:
theorem
IsSemisimpleRing.ideal_eq_span_idempotent
{R : Type u_2}
[Ring R]
[IsSemisimpleRing R]
(I : Ideal R)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
noncomputable instance
Module.End.divisionRing
{R : Type u_2}
[Ring R]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
[DecidableEq (End R M)]
[IsSimpleModule R M]
:
DivisionRing (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)
:
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)
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.