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

source

@[inline, reducible]

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

@[inline, reducible]

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

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

Nontrivial M

source

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

IsSimpleModule R M

source

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

IsSimpleModule R { x // x ∈ m } ↔ IsAtom m

source

theorem isSimpleModule_iff_isCoatom {R : Type u_1} [Ring R] {M : Type u_2} [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_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {A : Submodule R M} {B : Submodule R M} (hAB : A ≤ B) :

A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)

source

@[simp]

theorem IsSimpleModule.isAtom {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {m : Submodule R M} [hm : IsSimpleModule R { x // x ∈ m }] :

IsAtom m

source

theorem is_semisimple_of_sSup_simples_eq_top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (h : sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤) :

IsSemisimpleModule R M

source

theorem IsSemisimpleModule.sSup_simples_eq_top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :

sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤

source

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

IsSemisimpleModule R { x // x ∈ m }

Equations

@IsSemisimpleModule.is_semisimple_submodule = @IsSemisimpleModule.is_semisimple_submodule.proof_1

source

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

sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤ ↔ IsSemisimpleModule R M

source

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

source

def JordanHolderModule.Iso {R : Type u_1} [Ring R] {M : Type u_2} [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 // x ∈ X.snd } ⧸ Submodule.comap (Submodule.subtype X.snd) X.fst) ≃ₗ[R] { x // x ∈ Y.snd } ⧸ Submodule.comap (Submodule.subtype Y.snd) Y.fst)

Instances For

source

theorem JordanHolderModule.iso_symm {R : Type u_1} [Ring R] {M : Type u_2} [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

source

theorem JordanHolderModule.iso_trans {R : Type u_1} [Ring R] {M : Type u_2} [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

source

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

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

source

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

JordanHolderLattice (Submodule R M)

Equations

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