feat(ring_theory/simple_module): simple modules and Schur's Lemma (#5473

)

Defines `is_simple_module` in terms of `is_simple_lattice`
Proves Schur's Lemma
Defines `division ring` structure on the endomorphism ring of a simple module

src/linear_algebra/basic.lean

@@ -1374,6 +1374,9 @@ theorem ker_eq_top {f : M →ₗ[R] M₂} : ker f = ⊤ ↔ f = 0 :=
 lemma range_le_bot_iff (f : M →ₗ[R] M₂) : range f ≤ ⊥ ↔ f = 0 :=
 by rw [range_le_iff_comap]; exact ker_eq_top
 
+theorem range_eq_bot {f : M →ₗ[R] M₂} : range f = ⊥ ↔ f = 0 :=
+by rw [← range_le_bot_iff, le_bot_iff]
+
 lemma range_le_ker_iff {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} : range f ≤ ker g ↔ g.comp f = 0 :=
 ⟨λ h, ker_eq_top.1 $ eq_top_iff'.2 $ λ x, h $ mem_map_of_mem trivial,
  λ h x hx, mem_ker.2 $ exists.elim hx $ λ y ⟨_, hy⟩, by rw [←hy, ←comp_apply, h, zero_apply]⟩

src/ring_theory/simple_module.lean

@@ -0,0 +1,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