misc(linear_algebra, ring_theory): more simple facts about `is_simple…

…_module` and order on submodules (#16786)

The main result is `is_coatom_ker_of_surjective`, but I added various miscellaneous lemmas along the way

src/algebra/module/equiv.lean

@@ -340,13 +340,15 @@ omit module_M₃
 
 @[simp] lemma refl_symm [module R M] : (refl R M).symm = linear_equiv.refl R M := rfl
 
-@[simp] lemma self_trans_symm [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
-  f.trans f.symm = linear_equiv.refl R M :=
+include re₁₂ re₂₁ module_M₁ module_M₂
+@[simp] lemma self_trans_symm (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
+  f.trans f.symm = linear_equiv.refl R₁ M₁ :=
 by { ext x, simp }
 
-@[simp] lemma symm_trans_self [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
-  f.symm.trans f = linear_equiv.refl R M₂ :=
+@[simp] lemma symm_trans_self (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
+  f.symm.trans f = linear_equiv.refl R₂ M₂ :=
 by { ext x, simp }
+omit re₁₂ re₂₁ module_M₁ module_M₂
 
 @[simp, norm_cast] lemma refl_to_linear_map [module R M] :
   (linear_equiv.refl R M : M →ₗ[R] M) = linear_map.id :=

src/linear_algebra/basic.lean

@@ -808,6 +808,21 @@ lemma map_strict_mono_of_injective : strict_mono (map f) :=
 
 end galois_coinsertion
 
+section order_iso
+omit sc
+include σ₁₂ σ₂₁
+variables [semilinear_equiv_class F σ₁₂ M M₂]
+
+/-- A linear isomorphism induces an order isomorphism of submodules. -/
+@[simps symm_apply apply] def order_iso_map_comap (f : F) : submodule R M ≃o submodule R₂ M₂ :=
+{ to_fun := map f,
+  inv_fun := comap f,
+  left_inv := comap_map_eq_of_injective $ equiv_like.injective f,
+  right_inv := map_comap_eq_of_surjective $ equiv_like.surjective f,
+  map_rel_iff' := map_le_map_iff_of_injective $ equiv_like.injective f }
+
+end order_iso
+
 --TODO(Mario): is there a way to prove this from order properties?
 lemma map_inf_eq_map_inf_comap [ring_hom_surjective σ₁₂] {f : F}
   {p : submodule R M} {p' : submodule R₂ M₂} :
@@ -1963,6 +1978,16 @@ lemma comap_equiv_eq_map_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : submodule R
   K.comap (e : M →ₛₗ[τ₁₂] M₂) = K.map (e.symm : M₂ →ₛₗ[τ₂₁] M) :=
 (map_equiv_eq_comap_symm e.symm K).symm
 
+include τ₂₁
+lemma order_iso_map_comap_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : submodule R M) :
+  order_iso_map_comap e p = comap e.symm p :=
+p.map_equiv_eq_comap_symm _
+
+lemma order_iso_map_comap_symm_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : submodule R₂ M₂) :
+  (order_iso_map_comap e).symm p = map e.symm p :=
+p.comap_equiv_eq_map_symm _
+omit τ₂₁
+
 lemma comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) :
   comap fₗ qₗ ≤ comap (c • fₗ) qₗ :=
 begin

src/ring_theory/ideal/basic.lean

@@ -519,6 +519,10 @@ begin
   simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
 end
 
+/-- Ideals of a `division_ring` are a simple order. Thanks to the way abbreviations work, this
+automatically gives a `is_simple_module K` instance. -/
+instance : is_simple_order (ideal K) := ⟨eq_bot_or_top⟩
+
 lemma eq_bot_of_prime [h : I.is_prime] : I = ⊥ :=
 or_iff_not_imp_right.mp I.eq_bot_or_top h.1
 

src/ring_theory/simple_module.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson
 
 import linear_algebra.span
 import order.atoms
+import linear_algebra.isomorphisms
 
 /-!
 # Simple Modules
@@ -47,6 +48,9 @@ end⟩⟩
 
 variables {R} {M} {m : submodule R M} {N : Type*} [add_comm_group N] [module R N]
 
+lemma is_simple_module.congr (l : M ≃ₗ[R] N) [is_simple_module R N] : is_simple_module R M :=
+(submodule.order_iso_map_comap l).is_simple_order
+
 theorem is_simple_module_iff_is_atom :
   is_simple_module R m ↔ is_atom m :=
 begin
@@ -55,6 +59,14 @@ begin
   exact submodule.map_subtype.rel_iso m,
 end
 
+theorem is_simple_module_iff_is_coatom :
+  is_simple_module R (M ⧸ m) ↔ is_coatom m :=
+begin
+  rw ← set.is_simple_order_Ici_iff_is_coatom,
+  apply order_iso.is_simple_order_iff,
+  exact submodule.comap_mkq.rel_iso m,
+end
+
 namespace is_simple_module
 
 variable [hm : is_simple_module R m]
@@ -131,6 +143,13 @@ theorem bijective_of_ne_zero [is_simple_module R M] [is_simple_module R N]
   function.bijective f :=
 f.bijective_or_eq_zero.resolve_right h
 
+theorem is_coatom_ker_of_surjective [is_simple_module R N] {f : M →ₗ[R] N}
+  (hf : function.surjective f) : is_coatom f.ker :=
+begin
+  rw ←is_simple_module_iff_is_coatom,
+  exact is_simple_module.congr (f.quot_ker_equiv_of_surjective hf)
+end
+
 /-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/
 noncomputable instance _root_.module.End.division_ring
   [decidable_eq (module.End R M)] [is_simple_module R M] :