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 aDivisionRing
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
A module is simple when it has only two submodules, ⊥
and ⊤
.
Equations
- IsSimpleModule R M = IsSimpleOrder (Submodule R M)
Instances For
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
A ring is semisimple if it is semisimple as a module over itself.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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).
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.
A ring is a simple module over itself iff it is a division ring.
The annihilator of a semisimple module over a commutative ring is a radical ideal.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A module is semisimple iff it is generated by its simple submodules.
Alias of sSup_simples_eq_top_iff_isSemisimpleModule
.
A module is semisimple iff it is generated by its simple submodules.
A module generated by semisimple submodules is itself semisimple.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A finite product of semisimple rings is semisimple.
Equations
- ⋯ = ⋯
A binary product of semisimple rings is semisimple.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Schur's Lemma for linear maps between (possibly distinct) simple modules
Schur's Lemma makes the endomorphism ring of a simple module a division ring.
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
Equations
- One or more equations did not get rendered due to their size.