/
simple_module.lean
109 lines (90 loc) · 3.54 KB
/
simple_module.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
/-
Copyright (c) 2020 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors : Aaron Anderson
-/
import linear_algebra.basic
import order.atoms
/-!
# Simple Modules
## Main Definitions
* `is_simple_module` indicates that a module has no proper submodules
(the only submodules are `⊥` and `⊤`).
* 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
* Semisimple modules, Artin-Wedderburn Theory
* Unify with the work on Schur's Lemma in a category theory context
-/
variables (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M] [module R M]
/-- A module is simple when it has only two submodules, `⊥` and `⊤`. -/
abbreviation is_simple_module := (is_simple_lattice (submodule R M))
-- Making this an instance causes the linter to complain of "dangerous instances"
theorem is_simple_module.nontrivial [is_simple_module R M] : nontrivial M :=
⟨⟨0, begin
have h : (⊥ : submodule R M) ≠ ⊤ := bot_ne_top,
contrapose! h,
ext,
simp [submodule.mem_bot,submodule.mem_top, h x],
end⟩⟩
variables {R} {M} {N : Type*} [add_comm_group N] [module R N]
namespace linear_map
theorem injective_or_eq_zero [is_simple_module R M] (f : M →ₗ[R] N) :
function.injective f ∨ f = 0 :=
begin
rw [← ker_eq_bot, ← ker_eq_top],
apply eq_bot_or_eq_top,
end
theorem injective_of_ne_zero [is_simple_module R M] {f : M →ₗ[R] N} (h : f ≠ 0) :
function.injective f :=
f.injective_or_eq_zero.resolve_right h
theorem surjective_or_eq_zero [is_simple_module R N] (f : M →ₗ[R] N) :
function.surjective f ∨ f = 0 :=
begin
rw [← range_eq_top, ← range_eq_bot, or_comm],
apply eq_bot_or_eq_top,
end
theorem surjective_of_ne_zero [is_simple_module R N] {f : M →ₗ[R] N} (h : f ≠ 0) :
function.surjective f :=
f.surjective_or_eq_zero.resolve_right h
/-- Schur's Lemma for linear maps between (possibly distinct) simple modules -/
theorem bijective_or_eq_zero [is_simple_module R M] [is_simple_module R N]
(f : M →ₗ[R] N) :
function.bijective f ∨ f = 0 :=
begin
by_cases h : f = 0,
{ right,
exact h },
exact or.intro_left _ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩,
end
theorem bijective_of_ne_zero [is_simple_module R M] [is_simple_module R N]
{f : M →ₗ[R] N} (h : f ≠ 0):
function.bijective f :=
f.bijective_or_eq_zero.resolve_right h
/-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/
noncomputable instance [decidable_eq (module.End R M)] [is_simple_module R M] :
division_ring (module.End R M) :=
{ inv := λ f, if h : f = 0 then 0 else (linear_map.inverse f
(equiv.of_bijective _ (bijective_of_ne_zero h)).inv_fun
(equiv.of_bijective _ (bijective_of_ne_zero h)).left_inv
(equiv.of_bijective _ (bijective_of_ne_zero h)).right_inv),
exists_pair_ne := ⟨0, 1, begin
haveI := is_simple_module.nontrivial R M,
have h := exists_pair_ne M,
contrapose! h,
intros x y,
simp_rw [ext_iff, one_app, zero_apply] at h,
rw [← h x, h y],
end⟩,
mul_inv_cancel := begin
intros a a0,
change (a * (dite _ _ _)) = 1,
ext,
rw [dif_neg a0, mul_eq_comp, one_app, comp_apply],
exact (equiv.of_bijective _ (bijective_of_ne_zero a0)).right_inv x,
end,
inv_zero := dif_pos rfl,
.. (linear_map.endomorphism_ring : ring (module.End R M))}
end linear_map