Simple Modules #

Main Definitions #

is_simple_module indicates that a module has no proper submodules (the only submodules are ⊥ and ⊤).
is_semisimple_module indicates that every submodule has a complement, or equivalently, the module is a direct sum of simple modules.
A division_ring 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 division_ring structure on the endomorphism ring.

TODO #

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

source

def is_simple_module (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group M] [module R M] :

Prop

A module is simple when it has only two submodules, ⊥ and ⊤.

source

def is_semisimple_module (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group 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.

source

theorem is_simple_module.nontrivial (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group M] [module R M] [is_simple_module R M] :

nontrivial M

source

theorem is_simple_module_iff_is_atom {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {m : submodule R M} :

is_simple_module R ↥m ↔ is_atom m

source

@[simp]

theorem is_simple_module.is_atom {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {m : submodule R M} [hm : is_simple_module R ↥m] :

is_atom m

source

theorem is_semisimple_of_Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] (h : Sup {m : submodule R M | is_simple_module R ↥m} = ⊤) :

is_semisimple_module R M

source

theorem is_semisimple_module.Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] [is_semisimple_module R M] :

Sup {m : submodule R M | is_simple_module R ↥m} = ⊤

source

@[protected, instance]

def is_semisimple_module.is_semisimple_submodule {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] [is_semisimple_module R M] {m : submodule R M} :

is_semisimple_module R ↥m

source

theorem is_semisimple_iff_top_eq_Sup_simples {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] :

Sup {m : submodule R M | is_simple_module R ↥m} = ⊤ ↔ is_semisimple_module R M

source

theorem linear_map.injective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] (f : M →ₗ[R] N) :

function.injective ⇑f ∨ f = 0

source

theorem linear_map.injective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] {f : M →ₗ[R] N} (h : f ≠ 0) :

function.injective ⇑f

source

theorem linear_map.surjective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R N] (f : M →ₗ[R] N) :

function.surjective ⇑f ∨ f = 0

source

theorem linear_map.surjective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R N] {f : M →ₗ[R] N} (h : f ≠ 0) :

function.surjective ⇑f

source

theorem linear_map.bijective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] [is_simple_module R N] (f : M →ₗ[R] N) :

function.bijective ⇑f ∨ f = 0

Schur's Lemma for linear maps between (possibly distinct) simple modules

source

theorem linear_map.bijective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] [is_simple_module R N] {f : M →ₗ[R] N} (h : f ≠ 0) :

function.bijective ⇑f

source

@[protected, instance]

noncomputable def module.End.division_ring {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] [decidable_eq (module.End R M)] [is_simple_module R M] :

division_ring (module.End R M)

Schur's Lemma makes the endomorphism ring of a simple module a division ring.

Equations

module.End.division_ring = {add := ring.add module.End.ring, add_assoc := _, zero := ring.zero module.End.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul module.End.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg module.End.ring, sub := ring.sub module.End.ring, sub_eq_add_neg := _, zsmul := ring.zsmul module.End.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul module.End.ring, mul_assoc := _, one := ring.one module.End.ring, one_mul := _, mul_one := _, npow := ring.npow module.End.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := λ (f : module.End R M), dite (f = 0) (λ (h : f = 0), 0) (λ (h : ¬f = 0), linear_map.inverse f (equiv.of_bijective ⇑f _).inv_fun _ _), div := div_inv_monoid.div._default ring.mul module.End.division_ring._proof_22 ring.one module.End.division_ring._proof_23 module.End.division_ring._proof_24 ring.npow module.End.division_ring._proof_25 module.End.division_ring._proof_26 (λ (f : module.End R M), dite (f = 0) (λ (h : f = 0), 0) (λ (h : ¬f = 0), linear_map.inverse f (equiv.of_bijective ⇑f _).inv_fun _ _)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul module.End.division_ring._proof_28 ring.one module.End.division_ring._proof_29 module.End.division_ring._proof_30 ring.npow module.End.division_ring._proof_31 module.End.division_ring._proof_32 (λ (f : module.End R M), dite (f = 0) (λ (h : f = 0), 0) (λ (h : ¬f = 0), linear_map.inverse f (equiv.of_bijective ⇑f _).inv_fun _ _)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}