From 47a377d2aff88cd3bbfcbeb2994aca8e9626a095 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+dorhinj@users.noreply.github.com>
Date: Thu, 16 Aug 2018 12:09:33 +0100
Subject: [PATCH] refactor(group_theory/quotient_group): remove duplicate
 definition (#259)

---
 group_theory/coset.lean            | 101 +++++++----------------------
 group_theory/group_action.lean     |  27 ++++----
 group_theory/order_of_element.lean |  13 ++--
 group_theory/quotient_group.lean   |  85 +++++++++++++++---------
 group_theory/subgroup.lean         |   6 ++
 5 files changed, 105 insertions(+), 127 deletions(-)

diff --git a/group_theory/coset.lean b/group_theory/coset.lean
index 9f943c09fa410..9354cca14be3b 100644
--- a/group_theory/coset.lean
+++ b/group_theory/coset.lean
@@ -113,6 +113,8 @@ theorem normal_iff_eq_cosets : normal_subgroup s ↔ ∀ g, g *l s = s *r g :=
 
 end coset_subgroup
 
+namespace quotient_group
+
 def left_rel [group α] (s : set α) [is_subgroup s] : setoid α :=
 ⟨λ x y, x⁻¹ * y ∈ s,
   assume x, by simp [is_submonoid.one_mem],
@@ -123,30 +125,31 @@ def left_rel [group α] (s : set α) [is_subgroup s] : setoid α :=
   have x⁻¹ * y * (y⁻¹ * z) ∈ s, from is_submonoid.mul_mem hxy hyz,
   by simpa [mul_assoc] using this⟩
 
-def left_cosets [group α] (s : set α) [is_subgroup s] : Type* := quotient (left_rel s)
-
-namespace left_cosets
+/-- `quotient s` is the quotient type representing the left cosets of `s`.
+  If `s` is a normal subgroup, `quotient s` is a group -/
+def quotient [group α] (s : set α) [is_subgroup s] : Type* := quotient (left_rel s)
 
 variables [group α] {s : set α} [is_subgroup s]
 
-def mk (a : α) : left_cosets s :=
+def mk (a : α) : quotient s :=
 quotient.mk' a
 
-instance : has_coe α (left_cosets s) := ⟨mk⟩
+instance : has_coe α (quotient s) := ⟨mk⟩
 
-instance [group α] (s : set α) [is_subgroup s] : inhabited (left_cosets s) :=
-⟨((1 : α) : left_cosets s)⟩
+instance [group α] (s : set α) [is_subgroup s] : inhabited (quotient s) :=
+⟨((1 : α) : quotient s)⟩
 
-@[simp] protected lemma eq {a b : α} : (a : left_cosets s) = b ↔ a⁻¹ * b ∈ s :=
+protected lemma eq {a b : α} : (a : quotient s) = b ↔ a⁻¹ * b ∈ s :=
 quotient.eq'
 
-lemma eq_class_eq_left_coset [group α] (s : set α) [is_subgroup s] (g : α) : 
-  {x : α | (x : left_cosets s) = g} = left_coset g s :=
-set.ext $ λ z, by simp [eq_comm, mem_left_coset_iff]; refl
+lemma eq_class_eq_left_coset [group α] (s : set α) [is_subgroup s] (g : α) :
+  {x : α | (x : quotient s) = g} = left_coset g s :=
+set.ext $ λ z, by rw [mem_left_coset_iff, set.mem_set_of_eq, eq_comm, quotient_group.eq]
 
-end left_cosets
+end quotient_group
 
 namespace is_subgroup
+open quotient_group
 variables [group α] {s : set α}
 
 def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s :=
@@ -155,73 +158,19 @@ def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s :=
  λ ⟨x, hx⟩, subtype.eq $ by simp,
  λ ⟨g, hg⟩, subtype.eq $ by simp⟩
 
-local attribute [instance] left_rel
-
-noncomputable def group_equiv_left_cosets_times_subgroup (hs : is_subgroup s) :
-  α ≃ (left_cosets s × s) :=
-calc α ≃ Σ L : left_cosets s, {x : α // (x : left_cosets s)= L} :
-  equiv.equiv_fib left_cosets.mk
-    ... ≃ Σ L : left_cosets s, left_coset (quotient.out' L) s :
-  equiv.sigma_congr_right (λ L, 
-    begin rw ← left_cosets.eq_class_eq_left_coset, 
+noncomputable def group_equiv_quotient_times_subgroup (hs : is_subgroup s) :
+  α ≃ (quotient s × s) :=
+calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} :
+  equiv.equiv_fib quotient_group.mk
+    ... ≃ Σ L : quotient s, left_coset (quotient.out' L) s :
+  equiv.sigma_congr_right (λ L,
+    begin rw ← eq_class_eq_left_coset,
       show {x // quotient.mk' x = L} ≃ {x : α // quotient.mk' x = quotient.mk' _},
       simp [-quotient.eq']
     end)
-    ... ≃ Σ L : left_cosets s, s :
+    ... ≃ Σ L : quotient s, s :
   equiv.sigma_congr_right (λ L, left_coset_equiv_subgroup _)
-    ... ≃ (left_cosets s × s) :
+    ... ≃ (quotient s × s) :
   equiv.sigma_equiv_prod _ _
 
-end is_subgroup
-
-namespace left_cosets
-
-instance [group α] (s : set α) [normal_subgroup s] : group (left_cosets s) :=
-{ one := (1 : α),
-  mul := λ a b, quotient.lift_on₂' a b
-    (λ a b, ((a * b : α) : left_cosets s))
-  (λ a₁ a₂ b₁ b₂ hab₁ hab₂,
-      quot.sound
-    ((is_subgroup.mul_mem_cancel_left s (is_subgroup.inv_mem hab₂)).1
-        (by rw [mul_inv_rev, mul_inv_rev, ← mul_assoc (a₂⁻¹ * a₁⁻¹),
-          mul_assoc _ b₂, ← mul_assoc b₂, mul_inv_self, one_mul, mul_assoc (a₂⁻¹)];
-          exact normal_subgroup.normal _ hab₁ _))),
-  mul_assoc := λ a b c, quotient.induction_on₃' a b c 
-    (λ a b c, congr_arg mk (mul_assoc a b c)), 
-  one_mul := λ a, quotient.induction_on' a
-    (λ a, congr_arg mk (one_mul a)),
-  mul_one := λ a, quotient.induction_on' a
-    (λ a, congr_arg mk (mul_one a)),
-  inv := λ a, quotient.lift_on' a (λ a, ((a⁻¹ : α) : left_cosets s))
-    (λ a b hab, quotient.sound' begin
-      show a⁻¹⁻¹ * b⁻¹ ∈ s,
-      rw ← mul_inv_rev,
-      exact is_subgroup.inv_mem (is_subgroup.mem_norm_comm hab)
-    end),
-  mul_left_inv := λ a, quotient.induction_on' a
-    (λ a, congr_arg mk (mul_left_inv a)) }
-
-instance [group α] (s : set α) [normal_subgroup s] :
-  is_group_hom (mk : α → left_cosets s) := ⟨λ _ _, rfl⟩
-
-instance [comm_group α] (s : set α) [normal_subgroup s] : comm_group (left_cosets s) :=
-{ mul_comm := λ a b, quotient.induction_on₂' a b 
-    (λ a b, congr_arg mk (mul_comm a b)),
-  ..left_cosets.group s }
-
-@[simp] lemma coe_one [group α] (s : set α) [normal_subgroup s] : 
-  ((1 : α) : left_cosets s) = 1 := rfl
-
-@[simp] lemma coe_mul [group α] (s : set α) [normal_subgroup s] (a b : α) :
-  ((a * b : α) : left_cosets s) = a * b := rfl
-
-@[simp] lemma coe_inv [group α] (s : set α) [normal_subgroup s] (a : α) :
-  ((a⁻¹ : α) : left_cosets s) = a⁻¹ := rfl
-
-@[simp] lemma coe_pow [group α] (s : set α) [normal_subgroup s] (a : α) (n : ℕ) :
-  ((a ^ n : α) : left_cosets s) = a ^ n := @is_group_hom.pow _ _ _ _ mk _ a n
-
-@[simp] lemma coe_gpow [group α] (s : set α) [normal_subgroup s] (a : α) (n : ℤ) :
-  ((a ^ n : α) : left_cosets s) = a ^ n := @is_group_hom.gpow _ _ _ _ mk _ a n
-
-end left_cosets
\ No newline at end of file
+end is_subgroup
\ No newline at end of file
diff --git a/group_theory/group_action.lean b/group_theory/group_action.lean
index e56691e601768..3af46182245a1 100644
--- a/group_theory/group_action.lean
+++ b/group_theory/group_action.lean
@@ -14,7 +14,7 @@ class is_monoid_action [monoid α] (f : α → β → β) : Prop :=
 
 namespace is_monoid_action
 
-variables [monoid α] (f : α → β → β) [is_monoid_action f] 
+variables [monoid α] (f : α → β → β) [is_monoid_action f]
 
 def orbit (a : β) := set.range (λ x : α, f x a)
 
@@ -70,7 +70,7 @@ instance : is_group_hom (to_perm f) :=
 lemma bijective (g : α) : function.bijective (f g) :=
 (to_perm f g).bijective
 
-lemma orbit_eq_iff {f : α → β → β} [is_monoid_action f] {a b : β} : 
+lemma orbit_eq_iff {f : α → β → β} [is_monoid_action f] {a b : β} :
    orbit f a = orbit f b ↔ a ∈ orbit f b:=
 ⟨λ h, h ▸ mem_orbit_self _ _,
 λ ⟨x, (hx : f x b = a)⟩, set.ext (λ c, ⟨λ ⟨y, (hy : f y a = c)⟩, ⟨y * x,
@@ -87,21 +87,22 @@ instance (a : β) : is_subgroup (stabilizer f a) :=
   inv_mem := λ x (hx : f x a = a), show f x⁻¹ a = a,
     by rw [← hx, ← is_monoid_action.mul f, inv_mul_self, is_monoid_action.one f, hx] }
 
-noncomputable lemma orbit_equiv_left_cosets (a : β) :
-  orbit f a ≃ left_cosets (stabilizer f a) :=
-by letI := left_rel (stabilizer f a); exact
-equiv.symm (@equiv.of_bijective _ _ 
-  (λ x : left_cosets (stabilizer f a), quotient.lift_on x 
-    (λ x, (⟨f x a, mem_orbit _ _ _⟩ : orbit f a)) 
+open quotient_group
+
+noncomputable def orbit_equiv_quotient_stabilizer (a : β) :
+  orbit f a ≃ quotient (stabilizer f a) :=
+equiv.symm (@equiv.of_bijective _ _
+  (λ x : quotient (stabilizer f a), quotient.lift_on' x
+    (λ x, (⟨f x a, mem_orbit _ _ _⟩ : orbit f a))
     (λ g h (H : _ = _), subtype.eq $ (is_group_action.bijective f (g⁻¹)).1
       $ show f g⁻¹ (f g a) = f g⁻¹ (f h a),
-      by rw [← is_monoid_action.mul f, ← is_monoid_action.mul f, 
-        H, inv_mul_self, is_monoid_action.one f])) 
-⟨λ g h, quotient.induction_on₂ g h (λ g h H, quotient.sound $
-  have H : f g a = f h a := subtype.mk.inj H, 
+      by rw [← is_monoid_action.mul f, ← is_monoid_action.mul f,
+        H, inv_mul_self, is_monoid_action.one f]))
+⟨λ g h, quotient.induction_on₂' g h (λ g h H, quotient.sound' $
+  have H : f g a = f h a := subtype.mk.inj H,
   show f (g⁻¹ * h) a = a,
   by rw [is_monoid_action.mul f, ← H, ← is_monoid_action.mul f, inv_mul_self,
     is_monoid_action.one f]),
-  λ ⟨b, ⟨g, hgb⟩⟩, ⟨⟦g⟧, subtype.eq hgb⟩⟩)
+  λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩)
 
 end is_group_action
\ No newline at end of file
diff --git a/group_theory/order_of_element.lean b/group_theory/order_of_element.lean
index 573cf5b05c3db..01863ee4250aa 100644
--- a/group_theory/order_of_element.lean
+++ b/group_theory/order_of_element.lean
@@ -121,20 +121,21 @@ end
 
 section classical
 local attribute [instance] classical.prop_decidable
+open quotient_group
 
 /- TODO: use cardinal theory, introduce `card : set α → ℕ`, or setup decidability for cosets -/
 lemma order_of_dvd_card_univ : order_of a ∣ fintype.card α :=
-have ft_prod : fintype (left_cosets (gpowers a) × (gpowers a)),
-  from fintype.of_equiv α (gpowers.is_subgroup a).group_equiv_left_cosets_times_subgroup,
+have ft_prod : fintype (quotient (gpowers a) × (gpowers a)),
+  from fintype.of_equiv α (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup,
 have ft_s : fintype (gpowers a),
   from @fintype.fintype_prod_right _ _ _ ft_prod _,
-have ft_cosets : fintype (left_cosets (gpowers a)),
+have ft_cosets : fintype (quotient (gpowers a)),
   from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, is_submonoid.one_mem (gpowers a)⟩⟩,
-have ft : fintype (left_cosets (gpowers a) × (gpowers a)),
+have ft : fintype (quotient (gpowers a) × (gpowers a)),
   from @prod.fintype _ _ ft_cosets ft_s,
 have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
   from calc fintype.card α = @fintype.card _ ft_prod :
-      @fintype.card_congr _ _ _ ft_prod (gpowers.is_subgroup a).group_equiv_left_cosets_times_subgroup
+      @fintype.card_congr _ _ _ ft_prod (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup
     ... = @fintype.card _ (@prod.fintype _ _ ft_cosets ft_s) :
       congr_arg (@fintype.card _) $ subsingleton.elim _ _
     ... = @fintype.card _ ft_cosets * @fintype.card _ ft_s :
@@ -142,7 +143,7 @@ have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
 have eq₂ : order_of a = @fintype.card _ ft_s,
   from calc order_of a = _ : order_eq_card_range_gpow
     ... = _ : congr_arg (@fintype.card _) $ subsingleton.elim _ _,
-dvd.intro (@fintype.card (left_cosets (gpowers a)) ft_cosets) $
+dvd.intro (@fintype.card (quotient (gpowers a)) ft_cosets) $
   by rw [eq₁, eq₂, mul_comm]
 
 end classical
diff --git a/group_theory/quotient_group.lean b/group_theory/quotient_group.lean
index e8aca2e90fa45..1e9de543767f3 100644
--- a/group_theory/quotient_group.lean
+++ b/group_theory/quotient_group.lean
@@ -11,58 +11,79 @@ universes u v
 
 variables {G : Type u} [group G] (N : set G) [normal_subgroup N] {H : Type v} [group H]
 
-local attribute [instance] left_rel normal_subgroup.to_is_subgroup
-
-definition quotient_group := left_cosets N
-
-local notation ` Q ` := quotient_group N
-
-instance : group Q := left_cosets.group N
-
-namespace group.quotient
-
-instance inhabited : inhabited Q := ⟨1⟩
-
-def mk : G → Q := λ g, ⟦g⟧
-
-instance is_group_hom_quotient_mk : is_group_hom (mk N) := by refine {..}; intros; refl
+namespace quotient_group
+
+instance : group (quotient N) :=
+{ one := (1 : G),
+  mul := λ a b, quotient.lift_on₂' a b
+    (λ a b, ((a * b : G) : quotient N))
+  (λ a₁ a₂ b₁ b₂ hab₁ hab₂,
+      quot.sound
+    ((is_subgroup.mul_mem_cancel_left N (is_subgroup.inv_mem hab₂)).1
+        (by rw [mul_inv_rev, mul_inv_rev, ← mul_assoc (a₂⁻¹ * a₁⁻¹),
+          mul_assoc _ b₂, ← mul_assoc b₂, mul_inv_self, one_mul, mul_assoc (a₂⁻¹)];
+          exact normal_subgroup.normal _ hab₁ _))),
+  mul_assoc := λ a b c, quotient.induction_on₃' a b c
+    (λ a b c, congr_arg mk (mul_assoc a b c)),
+  one_mul := λ a, quotient.induction_on' a
+    (λ a, congr_arg mk (one_mul a)),
+  mul_one := λ a, quotient.induction_on' a
+    (λ a, congr_arg mk (mul_one a)),
+  inv := λ a, quotient.lift_on' a (λ a, ((a⁻¹ : G) : quotient N))
+    (λ a b hab, quotient.sound' begin
+      show a⁻¹⁻¹ * b⁻¹ ∈ N,
+      rw ← mul_inv_rev,
+      exact is_subgroup.inv_mem (is_subgroup.mem_norm_comm hab)
+    end),
+  mul_left_inv := λ a, quotient.induction_on' a
+    (λ a, congr_arg mk (mul_left_inv a)) }
+
+instance : is_group_hom (mk : G → quotient N) := ⟨λ _ _, rfl⟩
+
+instance {G : Type*} [comm_group G] (s : set G) [is_subgroup s] : comm_group (quotient s) :=
+{ mul_comm := λ a b, quotient.induction_on₂' a b
+    (λ a b, congr_arg mk (mul_comm a b)),
+  ..@quotient_group.group _ _ s (normal_subgroup_of_comm_group s) }
+
+@[simp] lemma coe_one : ((1 : G) : quotient N) = 1 := rfl
+@[simp] lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl
+@[simp] lemma coe_inv (a : G) : ((a⁻¹ : G) : quotient N) = a⁻¹ := rfl
+@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : quotient N) = a ^ n :=
+@is_group_hom.pow _ _ _ _ mk _ a n
+
+@[simp] lemma coe_gpow (a : G) (n : ℤ) : ((a ^ n : G) : quotient N) = a ^ n :=
+@is_group_hom.gpow _ _ _ _ mk _ a n
+
+local notation ` Q ` := quotient N
+
+instance is_group_hom_quotient_group_mk : is_group_hom (mk : G → Q) :=
+by refine {..}; intros; refl
 
 def lift (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (q : Q) : H :=
-q.lift_on φ $ assume a b (hab : a⁻¹ * b ∈ N),
+q.lift_on' φ $ assume a b (hab : a⁻¹ * b ∈ N),
 (calc φ a = φ a * 1           : by simp
 ...       = φ a * φ (a⁻¹ * b) : by rw HN (a⁻¹ * b) hab
 ...       = φ (a * (a⁻¹ * b)) : by rw is_group_hom.mul φ a (a⁻¹ * b)
 ...       = φ b               : by simp)
 
 @[simp] lemma lift_mk {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN ⟦g⟧ = φ g := rfl
+  lift N φ HN (g : Q) = φ g := rfl
 
 @[simp] lemma lift_mk' {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (mk N g) = φ g := rfl
+  lift N φ HN (mk g : Q) = φ g := rfl
 
 variables (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1)
 
 instance is_group_hom_quotient_lift  :
   is_group_hom (lift N φ HN) :=
-⟨λ q r, quotient.induction_on₂ q r $ λ a b,
+⟨λ q r, quotient.induction_on₂' q r $ λ a b,
   show φ (a * b) = φ a * φ b, from is_group_hom.mul φ a b⟩
 
 open function is_group_hom
 
 lemma injective_ker_lift : injective (lift (ker φ) φ $ λ x h, (mem_ker φ).1 h) :=
-assume a b, quotient.induction_on₂ a b $ assume a b (h : φ a = φ b), quotient.sound $
+assume a b, quotient.induction_on₂' a b $ assume a b (h : φ a = φ b), quotient.sound' $
 show a⁻¹ * b ∈ ker φ, by rw [mem_ker φ,
   is_group_hom.mul φ, ← h, is_group_hom.inv φ, inv_mul_self]
 
-end group.quotient
-
-namespace group
-variables {cG : Type u} [comm_group cG] (cN : set cG) [normal_subgroup cN]
-
-instance : comm_group (quotient_group cN) :=
-{ mul_comm := λ a b, quotient.induction_on₂ a b $ λ g h,
-    show ⟦g * h⟧ = ⟦h * g⟧,
-    by rw [mul_comm g h],
-  ..left_cosets.group cN }
-
-end group
+end quotient_group
diff --git a/group_theory/subgroup.lean b/group_theory/subgroup.lean
index 3df4714570abc..80a5c25aef375 100644
--- a/group_theory/subgroup.lean
+++ b/group_theory/subgroup.lean
@@ -189,6 +189,12 @@ attribute [to_additive normal_add_subgroup.to_is_add_subgroup] normal_subgroup.t
 attribute [to_additive normal_add_subgroup.normal] normal_subgroup.normal
 attribute [to_additive normal_add_subgroup.mk] normal_subgroup.mk
 
+@[to_additive normal_add_subgroup_of_add_comm_group]
+lemma normal_subgroup_of_comm_group [comm_group α] (s : set α) [hs : is_subgroup s] :
+  normal_subgroup s :=
+{ normal := λ n hn g, by rwa [mul_right_comm, mul_right_inv, one_mul],
+  ..hs }
+
 instance additive.normal_add_subgroup [group α]
   (s : set α) [normal_subgroup s] : @normal_add_subgroup (additive α) _ s :=
 ⟨@normal_subgroup.normal _ _ _ _⟩