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.

TODO

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

@[inline, reducible]

abbrev IsSimpleModule (R : Type u_2) [Ring R] (M : Type u_3) [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)

@[inline, reducible]

abbrev IsSemisimpleModule (R : Type u_2) [Ring R] (M : Type u_3) [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)

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

theorem IsSimpleModule.congr {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [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_3} [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_3} [AddCommGroup M] [Module R M] {A : Submodule R M} {B : Submodule R M} (hAB : A ≤ B) : A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap (Submodule.subtype B) A)

@[simp]

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

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

theorem IsSemisimpleModule.sSup_simples_eq_top {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤

instance IsSemisimpleModule.is_semisimple_submodule {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} : IsSemisimpleModule R ↥m

Equations

• (_ : IsSemisimpleModule R ↥m) = (_ : ComplementedLattice (Submodule R ↥m))

theorem is_semisimple_iff_top_eq_sSup_simples {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] : sSup {m : Submodule R M | IsSimpleModule R ↥m} = ⊤ ↔ IsSemisimpleModule R M

theorem isSemisimpleModule_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_3} [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

theorem isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_3} [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_3} [AddCommGroup M] [Module R M] {p : ι → Submodule R M} (hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)) (hp' : ⨆ (i : ι), p i = ⊤) : IsSemisimpleModule R M

theorem LinearMap.injective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [AddCommGroup M] [Module R M] {N : Type u_4} [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_3} [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

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

def JordanHolderModule.Iso {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] (X : Submodule R M × Submodule R M) (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 (Submodule.subtype X.2) X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap (Submodule.subtype Y.2) Y.1)

theorem JordanHolderModule.iso_symm {R : Type u_2} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {X : Submodule R M × Submodule R M} {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_3} [AddCommGroup M] [Module R M] {X : Submodule R M × Submodule R M} {Y : Submodule R M × Submodule R M} {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_3} [AddCommGroup M] [Module R M] {X : Submodule R M} {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_3} [AddCommGroup M] [Module R M] : JordanHolderLattice (Submodule R M)

Equations

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