Simple Modules #
Main Definitions #
is_simple_moduleindicates that a module has no proper submodules (the only submodules are⊥and⊤).is_semisimple_moduleindicates that every submodule has a complement, or equivalently, the module is a direct sum of simple modules.- A
division_ringstructure on the endomorphism ring of a simple module.
Main Results #
- Schur's Lemma:
bijective_or_eq_zeroshows that a linear map between simple modules is either bijective or 0, leading to adivision_ringstructure on the endomorphism ring.
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 ⊤.
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.
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] :
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
@[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
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} = ⊤) :
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] :
@[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} :
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
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
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) :
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
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) :
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
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) :
@[instance]
def
linear_map.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
- linear_map.module.End.division_ring = {add := ring.add linear_map.endomorphism_ring, add_assoc := _, zero := ring.zero linear_map.endomorphism_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul linear_map.endomorphism_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg linear_map.endomorphism_ring, sub := ring.sub linear_map.endomorphism_ring, sub_eq_add_neg := _, gsmul := ring.gsmul linear_map.endomorphism_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul linear_map.endomorphism_ring, mul_assoc := _, one := ring.one linear_map.endomorphism_ring, one_mul := _, mul_one := _, npow := ring.npow linear_map.endomorphism_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 linear_map.module.End.division_ring._proof_21 ring.one linear_map.module.End.division_ring._proof_22 linear_map.module.End.division_ring._proof_23 ring.npow linear_map.module.End.division_ring._proof_24 linear_map.module.End.division_ring._proof_25 (λ (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 := _, gpow := div_inv_monoid.gpow._default ring.mul linear_map.module.End.division_ring._proof_27 ring.one linear_map.module.End.division_ring._proof_28 linear_map.module.End.division_ring._proof_29 ring.npow linear_map.module.End.division_ring._proof_30 linear_map.module.End.division_ring._proof_31 (λ (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 _ _)), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}