From 5ffcd2a2d812dca5a5d24d18ce963102d354f515 Mon Sep 17 00:00:00 2001
From: Haitao Zhang <zhtprog@gmail.com>
Date: Wed, 15 Jul 2015 19:36:18 -0700
Subject: [PATCH] feat(library/algebra/group): add definitions and lemmas of
 conjugation

---
 library/algebra/group.lean | 48 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index f5a8d180c..9e68e68b9 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -281,6 +281,54 @@ section group
   theorem mul_eq_one_iff_mul_eq_one (a b : A) : a * b = 1 ↔ b * a = 1 :=
   iff.intro !mul_eq_one_of_mul_eq_one !mul_eq_one_of_mul_eq_one
 
+  definition conj_by (g a : A) := g * a * g⁻¹
+  definition is_conjugate (a b : A) := ∃ x, conj_by x b = a
+
+  local infixl `~` := is_conjugate
+  local infixr `∘c`:55 := conj_by
+
+  lemma conj_compose (f g a : A) : f ∘c g ∘c a = f*g ∘c a :=
+      calc f ∘c g ∘c a = f * (g * a * g⁻¹) * f⁻¹ : rfl
+      ... = f * (g * a) * g⁻¹ * f⁻¹ : mul.assoc
+      ... = f * g * a * g⁻¹ * f⁻¹ : mul.assoc
+      ... = f * g * a * (g⁻¹ * f⁻¹) : mul.assoc
+      ... = f * g * a * (f * g)⁻¹ : mul_inv
+  lemma conj_id (a : A) : 1 ∘c a = a :=
+      calc 1 * a * 1⁻¹ = a * 1⁻¹ : one_mul
+      ... = a * 1 : one_inv
+      ... = a : mul_one
+  lemma conj_one (g : A) : g ∘c 1 = 1 :=
+      calc g * 1 * g⁻¹ = g * g⁻¹ : mul_one
+      ... = 1 : mul.right_inv
+  lemma conj_inv_cancel (g : A) : ∀ a, g⁻¹ ∘c g ∘c a = a :=
+      assume a, calc
+      g⁻¹ ∘c g ∘c a = g⁻¹*g ∘c a : conj_compose
+      ... = 1 ∘c a : mul.left_inv
+      ... = a : conj_id
+
+  lemma conj_inv (g : A) : ∀ a, (g ∘c a)⁻¹ = g ∘c a⁻¹ :=
+    take a, calc
+    (g * a * g⁻¹)⁻¹ = g⁻¹⁻¹ * (g * a)⁻¹   : mul_inv
+                ... = g⁻¹⁻¹ * (a⁻¹ * g⁻¹) : mul_inv
+                ... = g⁻¹⁻¹ * a⁻¹ * g⁻¹   : mul.assoc
+                ... = g * a⁻¹ * g⁻¹       : inv_inv
+
+  lemma is_conj.refl (a : A) : a ~ a := exists.intro 1 (conj_id a)
+
+  lemma is_conj.symm (a b : A) : a ~ b → b ~ a :=
+      assume Pab, obtain x (Pconj : x ∘c b = a), from Pab,
+      assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, from (congr_arg2 conj_by (eq.refl x⁻¹) Pconj),
+      exists.intro x⁻¹ (eq.symm (conj_inv_cancel x b ▸ Pxinv))
+
+  lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c :=
+      assume Pab, assume Pbc,
+      obtain x (Px : x ∘c b = a), from Pab,
+      obtain y (Py : y ∘c c = b), from Pbc,
+      exists.intro (x*y) (calc
+      x*y ∘c c = x ∘c y ∘c c : conj_compose
+      ... = x ∘c b : Py
+      ... = a : Px)
+
   definition group.to_left_cancel_semigroup [trans-instance] [coercion] [reducible] :
     left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,