Simple Modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[reducible]

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

@[reducible]

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.congr {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] (l : M ≃ₗ[R] N) [is_simple_module R N] :

is_simple_module R 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

theorem is_simple_module_iff_is_coatom {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 ⧸ m) ↔ is_coatom m

source

theorem covby_iff_quot_is_simple {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {A B : submodule R M} (hAB : A ≤ B) :

A ⋖ B ↔ is_simple_module R (↥B ⧸ submodule.comap B.subtype A)

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 : has_Sup.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] :

has_Sup.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] :

has_Sup.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

theorem linear_map.is_coatom_ker_of_surjective {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} (hf : function.surjective ⇑f) :

is_coatom (linear_map.ker 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 := _, int_cast := ring.int_cast module.End.ring, nat_cast := ring.nat_cast module.End.ring, one := ring.one module.End.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul module.End.ring, mul_assoc := _, 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_26 ring.one module.End.division_ring._proof_27 module.End.division_ring._proof_28 ring.npow module.End.division_ring._proof_29 module.End.division_ring._proof_30 (λ (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_32 ring.one module.End.division_ring._proof_33 module.End.division_ring._proof_34 ring.npow module.End.division_ring._proof_35 module.End.division_ring._proof_36 (λ (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 := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (module.End R M)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (module.End R M)), qsmul_eq_mul' := _}

source

@[protected, instance]

def jordan_holder_module {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] :

jordan_holder_lattice (submodule R M)

Equations

jordan_holder_module = {is_maximal := covby (preorder.to_has_lt (submodule R M)), lt_of_is_maximal := _, sup_eq_of_is_maximal := _, is_maximal_inf_left_of_is_maximal_sup := _, iso := λ (X Y : submodule R M × submodule R M), nonempty ((↥(X.snd) ⧸ submodule.comap X.snd.subtype X.fst) ≃ₗ[R] ↥(Y.snd) ⧸ submodule.comap Y.snd.subtype Y.fst), iso_symm := _, iso_trans := _, second_iso := _}