feat(group_theory/conjugates) : define conjugates (#1029)

* feat(algebra/order_functions): generalize strict_mono.monotone (#1022)

* moving stuff to where it belongs

* removed unecessary import

* Changed to union

* Update src/group_theory/subgroup.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Stylistic changes

* Added authorship

* Moved mem_conjugates_of_set

* Authorship

* Trying fixes

* Putting everything in the right order

* removed import

src/algebra/group.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura
+Authors: Jeremy Avigad, Leonardo de Moura, Michael Howes
 
 Various multiplicative and additive structures.
 -/
@@ -605,6 +605,17 @@ def is_conj (a b : α) := ∃ c : α, c * a * c⁻¹ = b
 calc is_conj a 1 ↔ is_conj 1 a : ⟨is_conj_symm, is_conj_symm⟩
 ... ↔ a = 1 : is_conj_one_right
 
+@[simp] lemma conj_inv {a b : α} : (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹ :=
+begin
+  rw [mul_inv_rev _ b⁻¹, mul_inv_rev b _, inv_inv, mul_assoc],
+end
+
+@[simp] lemma conj_mul {a b c : α} : (b * a * b⁻¹) * (b * c * b⁻¹) = b * (a * c) * b⁻¹ :=
+begin
+  assoc_rw inv_mul_cancel_right,
+  repeat {rw mul_assoc},
+end
+
 @[simp] lemma is_conj_iff_eq {α : Type*} [comm_group α] {a b : α} : is_conj a b ↔ a = b :=
 ⟨λ ⟨c, hc⟩, by rw [← hc, mul_right_comm, mul_inv_self, one_mul], λ h, by rw h⟩
 

src/group_theory/subgroup.lean

@@ -1,7 +1,8 @@
 /-
 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro
+Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro,
+  Michael Howes
 -/
 import group_theory.submonoid
 open set function
@@ -633,6 +634,98 @@ attribute [to_additive is_add_subgroup.trivial_eq_closure] is_subgroup.trivial_e
 
 end is_subgroup
 
+/-The normal closure of a set s is the subgroup closure of all the conjugates of
+elements of s. It is the smallest normal subgroup containing s. -/
+
+namespace group
+variables {s : set α} [group α]
+
+/-- Given an element a, conjugates a is the set of conjugates. -/
+def conjugates (a : α) : set α := {b | is_conj a b}
+
+lemma mem_conjugates_self {a : α} : a ∈ conjugates a := is_conj_refl _
+
+/-- Given a set s, conjugates_of_set s is the set of all conjugates of
+the elements of s. -/
+def conjugates_of_set (s : set α) : set α := ⋃ a ∈ s, conjugates a
+
+lemma mem_conjugates_of_set_iff {x : α} : x ∈ conjugates_of_set s ↔ ∃ a : α, a ∈ s ∧ is_conj a x :=
+set.mem_bUnion_iff
+
+theorem subset_conjugates_of_set : s ⊆ conjugates_of_set s :=
+λ (x : α) (h : x ∈ s), mem_conjugates_of_set_iff.2 ⟨x, h, is_conj_refl _⟩
+
+theorem conjugates_of_set_mono {s t : set α} (h : s ⊆ t) :
+  conjugates_of_set s ⊆ conjugates_of_set t :=
+set.bUnion_subset_bUnion_left h
+
+lemma conjugates_subset {t : set α} [normal_subgroup t] {a : α} (h : a ∈ t) : conjugates a ⊆ t :=
+λ x ⟨c,w⟩,
+begin
+  have H := normal_subgroup.normal a h c,
+  rwa ←w,
+end
+
+theorem conjugates_of_set_subset {s t : set α} [normal_subgroup t] (h : s ⊆ t) :
+  conjugates_of_set s ⊆ t :=
+set.bUnion_subset (λ x H, conjugates_subset (h H))
+
+/-- The set of conjugates of s is closed under conjugation. -/
+lemma conj_mem_conjugates_of_set {x c : α} :
+  x ∈ conjugates_of_set s → (c * x * c⁻¹ ∈ conjugates_of_set s) :=
+λ H,
+begin
+  rcases (mem_conjugates_of_set_iff.1 H) with ⟨a,h₁,h₂⟩,
+  exact mem_conjugates_of_set_iff.2 ⟨a, h₁, is_conj_trans h₂ ⟨c,rfl⟩⟩,
+end
+
+/-- The normal closure of a set s is the subgroup closure of all the conjugates of
+elements of s. It is the smallest normal subgroup containing s. -/
+def normal_closure (s : set α) : set α := closure (conjugates_of_set s)
+
+theorem conjugates_of_set_subset_normal_closure : conjugates_of_set s ⊆ normal_closure s :=
+subset_closure
+
+theorem subset_normal_closure : s ⊆ normal_closure s :=
+set.subset.trans subset_conjugates_of_set conjugates_of_set_subset_normal_closure
+
+/-- The normal closure of a set is a subgroup. -/
+instance normal_closure.is_subgroup (s : set α) : is_subgroup (normal_closure s) :=
+closure.is_subgroup (conjugates_of_set s)
+
+/-- The normal closure of s is a normal subgroup. -/
+instance normal_closure.is_normal : normal_subgroup (normal_closure s) :=
+⟨ λ n h g,
+begin
+  induction h with x hx x hx ihx x y hx hy ihx ihy,
+  {exact (conjugates_of_set_subset_normal_closure (conj_mem_conjugates_of_set hx))},
+  {simpa using (normal_closure.is_subgroup s).one_mem},
+  {rw ←conj_inv,
+   exact (is_subgroup.inv_mem ihx)},
+  {rw ←conj_mul,
+   exact (is_submonoid.mul_mem ihx ihy)},
+end ⟩
+
+/-- The normal closure of s is the smallest normal subgroup containing s. -/
+theorem normal_closure_subset {s t : set α} [normal_subgroup t] (h : s ⊆ t) :
+  normal_closure s ⊆ t :=
+λ a w,
+begin
+  induction w with x hx x hx ihx x y hx hy ihx ihy,
+  {exact (conjugates_of_set_subset h $ hx)},
+  {exact is_submonoid.one_mem t},
+  {exact is_subgroup.inv_mem ihx},
+  {exact is_submonoid.mul_mem ihx ihy}
+end
+
+lemma normal_closure_subset_iff {s t : set α} [normal_subgroup t] : s ⊆ t ↔ normal_closure s ⊆ t :=
+⟨normal_closure_subset, set.subset.trans (subset_normal_closure)⟩
+
+theorem normal_closure_mono {s t : set α} : s ⊆ t → normal_closure s ⊆ normal_closure t :=
+λ h, normal_closure_subset (set.subset.trans h (subset_normal_closure))
+
+end group
+
 section simple_group
 
 class simple_group (α : Type*) [group α] : Prop :=