hall_witt.lean

namespace hall_witt

class group (G : Type) :=
(mul : G → G → G)
(mul_assoc : ∀ (a b c : G), mul (mul a b) c = mul a (mul b c))
(one : G)
(one_mul : ∀ (a : G), mul one a = a)
(mul_one : ∀ (a : G), mul a one = a)
(inv : G → G)
(mul_left_inv : ∀ (a : G), mul (inv a) a = one)

instance {G} [group G] : has_one G := ⟨group.one _⟩
instance {G} [group G] : has_mul G := ⟨group.mul⟩
instance {G} [group G] : has_inv G := ⟨group.inv⟩

lemma group.uniq_id {G} [group G] : ∀ g h : G, g * h = g → h = 1 :=
λ g h hyp, calc h   = 1 * h         : eq.symm $ group.one_mul _
                ... = (g⁻¹ * g) * h : by { congr, symmetry, apply group.mul_left_inv }
                ... = g⁻¹ * (g * h) : group.mul_assoc _ _ _
                ... = g⁻¹ * g       : congr_arg _ hyp
                ... = 1             : group.mul_left_inv _

lemma group.mul_right_inv {G} [group G] : ∀ (a : G), a * a⁻¹ = 1 :=
λ a, group.uniq_id (a * a⁻¹) (a * a⁻¹) $ eq.symm $
  calc a * a⁻¹ = a * (1 * a⁻¹)         : congr_arg _ $ eq.symm $ group.one_mul a⁻¹
      ...     = a * ((a⁻¹ * a) * a⁻¹) : by { congr, symmetry, apply group.mul_left_inv }
      ...     = a * (a⁻¹ * (a * a⁻¹)) : by { apply congr_arg, apply group.mul_assoc }
      ...     = (a * a⁻¹) * (a * a⁻¹) : eq.symm $ group.mul_assoc _ _ _

lemma group.inv_unique {G} [group G] : ∀ x x' : G, x' * x = 1 → x' = x⁻¹ :=
λ x x' hyp, calc x'  = x' * 1         : eq.symm $ group.mul_one x'
                 ... = x' * (x * x⁻¹) : congr_arg _ $ eq.symm $ group.mul_right_inv x
                 ... = (x' * x) * x⁻¹ : eq.symm $ group.mul_assoc _ _ _
                 ... = 1 * x⁻¹        : by { congr, assumption }
                 ... = x⁻¹            : group.one_mul _

lemma group.mul_inv_rev {G} [group G] : ∀ x y : G, (x * y)⁻¹ = y⁻¹ * x⁻¹ := 
λ x y, eq.symm $ group.inv_unique (x * y) (y⁻¹ * x⁻¹) $
  calc y⁻¹ * x⁻¹ * (x * y) = y⁻¹ * (x⁻¹ * (x * y)) : group.mul_assoc _ _ _
       ...                 = y⁻¹ * ((x⁻¹ * x) * y) : congr_arg _ $ eq.symm $ group.mul_assoc _ _ _
       ...                 = y⁻¹ * (1 * y)         : by { congr, apply group.mul_left_inv }
       ...                 = y⁻¹ * y               : congr_arg _ $ group.one_mul y
       ...                 = 1                     : group.mul_left_inv _

lemma group.inv_inv {G} [group G] : ∀ x : G, (x⁻¹)⁻¹ = x :=
λ _, eq.symm $ group.inv_unique _ _ $ group.mul_right_inv _

lemma group.inv_mul_cancel_left {G} [group G] : ∀ (a b : G), a⁻¹ * (a * b) = b :=
λ a b, calc a⁻¹ * (a * b) = (a⁻¹ * a) * b : eq.symm $ group.mul_assoc _ _ _
            ...           = 1 * b         : by { congr, apply group.mul_left_inv }
            ...           = b             : group.one_mul _

lemma group.mul_inv_cancel_left {G} [group G] : ∀ (a b : G), a * (a⁻¹ * b) = b :=
by { intros, have : ∀ c, a * c = a⁻¹⁻¹ * c, { intro, congr, rw group.inv_inv },
     rw this, apply group.inv_mul_cancel_left }

lemma group.mul_assoc' {G} [group G] : ∀ (a b c : G), (a * b) * c = a * (b * c) := group.mul_assoc

@[reducible]
def commutator {G} [group G] (h k : G) := h⁻¹ * k⁻¹ * h * k

notation `[` x `,` y `,` z `]` := commutator (commutator x y) z

@[reducible]
def conj {G} [group G] (x y : G) := y⁻¹ * x * y

instance conj_pow {G} [group G] : has_pow G G := ⟨conj⟩

lemma hall_witt {G} [group G] : ∀ x y z : G,
  [x, y⁻¹, z]^y * [y, z⁻¹, x]^z * [z, x⁻¹, y]^x = 1 :=
begin
  intros, dsimp [has_pow.pow, conj, commutator], 
  repeat { rw group.mul_inv_rev },
  repeat { rw group.inv_inv }, 
  repeat { rw group.mul_assoc' }, 
  repeat { rw group.inv_mul_cancel_left <|> rw group.mul_inv_cancel_left },
  apply group.mul_left_inv
end

end hall_witt

@[reducible]
def commutator {G} [group G] (h k : G) := h⁻¹ * k⁻¹ * h * k

notation `[` x `,` y `,` z `]` := commutator (commutator x y) z

@[reducible]
def conj {G} [group G] (x y : G) := y⁻¹ * x * y

instance conj_pow {G} [group G] : has_pow G G := ⟨conj⟩

lemma hall_witt {G} [group G] : ∀ x y z : G,
  [x, y⁻¹, z]^y * [y, z⁻¹, x]^z * [z, x⁻¹, y]^x = 1 :=
begin
  intros, dsimp [has_pow.pow, conj, commutator], 
  repeat { rw mul_inv_rev },
  repeat { rw inv_inv }, 
  repeat { rw mul_assoc }, 
  repeat { rw inv_mul_cancel_left <|> rw mul_inv_cancel_left },
  apply mul_left_inv
end