[Merged by Bors] - feat(algebra/module/composition_series): Jordan-Hölder for modules

src/order/atoms.lean

@@ -136,6 +136,28 @@ alias covby_top_iff ↔ covby.is_coatom is_coatom.covby_top
 
 end is_coatom
 
+section partial_order
+variables [partial_order α] {a b : α}
+
+@[simp] lemma set.Ici.is_atom_iff {b : set.Ici a} : is_atom b ↔ a ⋖ b :=
+begin
+  rw ←bot_covby_iff,
+  refine (set.ord_connected.apply_covby_apply_iff (order_embedding.subtype $ λ c, a ≤ c) _).symm,
+  simpa only [order_embedding.subtype_apply, subtype.range_coe_subtype] using set.ord_connected_Ici,
+end
+
+@[simp] lemma set.Iic.is_coatom_iff {a : set.Iic b} : is_coatom a ↔ ↑a ⋖ b :=
+begin
+  rw ←covby_top_iff,
+  refine (set.ord_connected.apply_covby_apply_iff (order_embedding.subtype $ λ c, c ≤ b) _).symm,
+  simpa only [order_embedding.subtype_apply, subtype.range_coe_subtype] using set.ord_connected_Iic,
+end
+
+lemma covby_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ is_atom (⟨b, h⟩ : set.Ici a) := by simp
+lemma covby_iff_coatom_Iic (h : a ≤ b) : a ⋖ b ↔ is_coatom (⟨a, h⟩ : set.Iic b) := by simp
+
+end partial_order
+
 section pairwise
 
 lemma is_atom.inf_eq_bot_of_ne [semilattice_inf α] [order_bot α] {a b : α}

src/ring_theory/simple_module.lean

@@ -3,10 +3,8 @@ 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.span
-import order.atoms
 import linear_algebra.isomorphisms
+import order.jordan_holder
 
 /-!
 # Simple Modules
@@ -67,6 +65,15 @@ begin
   exact submodule.comap_mkq.rel_iso m,
 end
 
+theorem covby_iff_quot_is_simple {A B : submodule R M} (hAB : A ≤ B) :
+  A ⋖ B ↔ is_simple_module R (B ⧸ submodule.comap B.subtype A) :=
+begin
+  set f : submodule R B ≃o set.Iic B := submodule.map_subtype.rel_iso B with hf,
+  rw [covby_iff_coatom_Iic hAB, is_simple_module_iff_is_coatom, ←order_iso.is_coatom_iff f, hf],
+  simp [-order_iso.is_coatom_iff, submodule.map_subtype.rel_iso, submodule.map_comap_subtype,
+    inf_eq_right.2 hAB],
+end
+
 namespace is_simple_module
 
 variable [hm : is_simple_module R m]
@@ -177,3 +184,15 @@ noncomputable instance _root_.module.End.division_ring
 .. (module.End.ring : ring (module.End R M))}
 
 end linear_map
+
+instance jordan_holder_module : jordan_holder_lattice (submodule R M) :=
+{ is_maximal                            := (⋖),
+  lt_of_is_maximal                      := λ x y, covby.lt,
+  sup_eq_of_is_maximal                  := λ x y z hxz hyz, wcovby.sup_eq hxz.wcovby hyz.wcovby,
+  is_maximal_inf_left_of_is_maximal_sup := λ A B, inf_covby_of_covby_sup_of_covby_sup_left,
+  iso                                   := λ X Y,
+    nonempty $ (X.2 ⧸ X.1.comap X.2.subtype) ≃ₗ[R] Y.2 ⧸ Y.1.comap Y.2.subtype,
+  iso_symm                              := λ A B ⟨f⟩, ⟨f.symm⟩,
+  iso_trans                             := λ A B C ⟨f⟩ ⟨g⟩, ⟨f.trans g⟩,
+  second_iso                            := λ A B h,
+    ⟨by { rw [sup_comm, inf_comm], exact (linear_map.quotient_inf_equiv_sup_quotient B A).symm }⟩}