feat(group_theory,linear_algebra): third isomorphism theorem for grou…

…ps and modules (#8203)

This PR proves the third isomorphism theorem for (additive) groups and modules, and also adds a few `simp` lemmas that I needed.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

docs/overview.yaml

@@ -33,7 +33,9 @@ General algebra:
     subgroup: 'subgroup'
     subgroup generated by a subset: 'subgroup.closure'
     quotient group: 'quotient_group.quotient.group'
-    first isomorphism theorem: 'quotient_add_group.quotient_ker_equiv_range'
+    first isomorphism theorem: 'quotient_group.quotient_ker_equiv_range'
+    second isomorphism theorem: 'quotient_group.quotient_inf_equiv_prod_normal_quotient'
+    third isomorphism theorem: 'quotient_group.quotient_quotient_equiv_quotient'
     abelianization: 'abelianization'
     free group: 'free_group'
     group action: 'mul_action'

src/group_theory/quotient_group.lean

@@ -28,14 +28,12 @@ proves Noether's first and second isomorphism theorems.
 * `quotient_inf_equiv_prod_normal_quotient`: Noether's second isomorphism theorem, an explicit
   isomorphism between `H/(H ∩ N)` and `(HN)/N` given a subgroup `H` and a normal subgroup `N` of a
   group `G`.
+* `quotient_group.quotient_quotient_equiv_quotient`: Noether's third isomorphism theorem,
+  the canonical isomorphism between `(G / M) / (M / N)` and `G / N`, where `N ≤ M`.
 
 ## Tags
 
 isomorphism theorems, quotient groups
-
-## TODO
-
-Noether's third isomorphism theorem
 -/
 
 universes u v
@@ -172,6 +170,16 @@ begin
   exact h hx,
 end
 
+@[simp, to_additive quotient_add_group.map_coe] lemma map_coe
+  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+  map N M f h ↑x = ↑(f x) :=
+lift_mk' _ _ x
+
+@[to_additive quotient_add_group.map_mk'] lemma map_mk'
+  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+  map N M f h (mk' _ x) = ↑(f x) :=
+quotient_group.lift_mk' _ _ x
+
 omit nN
 variables (φ : G →* H)
 
@@ -291,4 +299,55 @@ have φ_surjective : function.surjective φ := λ x, x.induction_on' $
 
 end snd_isomorphism_thm
 
+section third_iso_thm
+
+variables (M : subgroup G) [nM : M.normal]
+
+include nM nN
+
+@[to_additive quotient_add_group.map_normal]
+instance map_normal : (M.map (quotient_group.mk' N)).normal :=
+{ conj_mem := begin
+    rintro _ ⟨x, hx, rfl⟩ y,
+    refine induction_on' y (λ y, ⟨y * x * y⁻¹, subgroup.normal.conj_mem nM x hx y, _⟩),
+    simp only [mk'_apply, coe_mul, coe_inv]
+  end }
+
+variables (h : N ≤ M)
+
+/-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`. -/
+@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux
+"The map from the third isomorphism theorem for additive groups: `(A / N) / (M / N) → A / M`."]
+def quotient_quotient_equiv_quotient_aux :
+  quotient (M.map (mk' N)) →* quotient M :=
+lift (M.map (mk' N))
+  (map N M (monoid_hom.id G) h)
+  (by { rintro _ ⟨x, hx, rfl⟩, rw map_mk' N M _ _ x,
+        exact (quotient_group.eq_one_iff _).mpr hx })
+
+@[simp, to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe]
+lemma quotient_quotient_equiv_quotient_aux_coe (x : quotient_group.quotient N) :
+  quotient_quotient_equiv_quotient_aux N M h x = quotient_group.map N M (monoid_hom.id G) h x :=
+quotient_group.lift_mk' _ _ x
+
+@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe]
+lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) :
+  quotient_quotient_equiv_quotient_aux N M h (x : quotient_group.quotient N) =
+    x :=
+quotient_group.lift_mk' _ _ x
+
+/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃ G / M`. -/
+@[to_additive quotient_add_group.quotient_quotient_equiv_quotient
+"**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃ A / M`."]
+def quotient_quotient_equiv_quotient :
+  quotient_group.quotient (M.map (quotient_group.mk' N)) ≃* quotient_group.quotient M :=
+{ to_fun := quotient_quotient_equiv_quotient_aux N M h,
+  inv_fun := quotient_group.map _ _ (quotient_group.mk' N) (subgroup.le_comap_map _ _),
+  left_inv := λ x, quotient_group.induction_on' x $ λ x, quotient_group.induction_on' x $
+    λ x, by simp,
+  right_inv := λ x, quotient_group.induction_on' x $ λ x, by simp,
+  map_mul' := monoid_hom.map_mul _ }
+
+end third_iso_thm
+
 end quotient_group

src/linear_algebra/basic.lean

@@ -37,8 +37,9 @@ Many of the relevant definitions, including `module`, `submodule`, and `linear_m
 
 ## Main statements
 
-* The first and second isomorphism laws for modules are proved as `quot_ker_equiv_range` and
-  `quotient_inf_equiv_sup_quotient`.
+* The first, second and third isomorphism laws for modules are proved as
+  `linear_map.quot_ker_equiv_range`, `linear_map.quotient_inf_equiv_sup_quotient` and
+  `submodule.quotient_quotient_equiv_quotient`.
 
 ## Notations
 
@@ -2835,4 +2836,34 @@ instance : is_modular_lattice (submodule R M) :=
   apply z.sub_mem haz (xz hb),
 end⟩
 
+section third_iso_thm
+
+variables (S T : submodule R M) (h : S ≤ T)
+
+/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/
+def quotient_quotient_equiv_quotient_aux :
+  quotient (T.map S.mkq) →ₗ[R] quotient T :=
+liftq _ (mapq S T linear_map.id h)
+  (by { rintro _ ⟨x, hx, rfl⟩, rw [linear_map.mem_ker, mkq_apply, mapq_apply],
+        exact (quotient.mk_eq_zero _).mpr hx })
+
+@[simp] lemma quotient_quotient_equiv_quotient_aux_mk (x : S.quotient) :
+  quotient_quotient_equiv_quotient_aux S T h (quotient.mk x) = mapq S T linear_map.id h x :=
+liftq_apply _ _ _
+
+@[simp] lemma quotient_quotient_equiv_quotient_aux_mk_mk (x : M) :
+  quotient_quotient_equiv_quotient_aux S T h (quotient.mk (quotient.mk x)) = quotient.mk x :=
+by rw [quotient_quotient_equiv_quotient_aux_mk, mapq_apply, linear_map.id_apply]
+
+/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`. -/
+def quotient_quotient_equiv_quotient :
+  quotient (T.map S.mkq) ≃ₗ[R] quotient T :=
+{ to_fun := quotient_quotient_equiv_quotient_aux S T h,
+  inv_fun := mapq _ _ (mkq S) (le_comap_map _ _),
+  left_inv := λ x, quotient.induction_on' x $ λ x, quotient.induction_on' x $ λ x, by simp,
+  right_inv := λ x, quotient.induction_on' x $ λ x, by simp,
+  .. quotient_quotient_equiv_quotient_aux S T h }
+
+end third_iso_thm
+
 end submodule