group.lean

namespace hidden

  class group (α : Type) extends has_mul α, has_one α, has_inv α :=
    (mul_assoc : ∀(a b c : α), (a * b) * c = a * (b * c))
    (e_mul : ∀(x : α), 1 * x = x) 
    (mul_e : ∀(x : α), x * 1 = x) 
    (mul_right_inv : ∀(x : α), x * x⁻¹ = 1)

  namespace group
    variables {α : Type} [group α]

    -- --x =
    -- e * --x =
    -- (x * -x) * --x =
    -- x * (-x * --x) =
    -- x * e =
    -- x
    lemma inv_inv (x : α) : x⁻¹⁻¹ = x :=
    begin
      rw ← e_mul (x⁻¹⁻¹),
      rw ← mul_right_inv x,
      rw mul_assoc,
      rw mul_right_inv x⁻¹,
      rw mul_e,
    end

    -- -x * x =
    -- -x * --x =
    -- e
    lemma mul_left_inv (x : α) : x⁻¹ * x = 1 :=
    begin
      let hidden_part := x⁻¹,
      let hide_part : hidden_part = x⁻¹, reflexivity,
      rw ← hide_part,
      rw ← inv_inv x,
      rw hide_part,
      rw mul_right_inv,
    end

    lemma monomorphism₁ (m x y : α) : x = y → m * x = m * y :=
    begin intro p, rw p end

    -- m * x = m * y  ==
    -- m⁻¹ * (m * x) = m⁻¹ * (m * y)  ==
    -- (m⁻¹ * m) * x = (m⁻¹ * m) * y  ==
    -- 1 * x = 1 * y  ==
    -- x = y
    lemma monomorphism₂ (m x y : α) : m * x = m * y → x = y :=
      λp,
      let q₀ := monomorphism₁ m⁻¹ _ _ p in
      let q₁ := ((mul_assoc _ _ _).trans q₀).trans (mul_assoc _ _ _).symm in
      let q₂ : 1 * x = 1 * y := mul_left_inv m ▸ q₁ in
      let q₃ : x = y := (e_mul x).symm.trans (q₂.trans (e_mul y)) in
      q₃

    lemma monomorphism (m x y : α) : x = y ↔ m * x = m * y :=
      ⟨monomorphism₁ m x y, monomorphism₂ m x y⟩



  end group

  structure homomorphism α β [group α] [group β] :=
    (map : α → β)
    (mul_holds : ∀u v, map (u * v) = map u * map v)

  namespace homomorphism

    variables {α : Type} [group α]
    variables {β : Type} [group β]
    variables [H : homomorphism α β]

    -- h(G.e) =
    -- h(G.e) * H.e =
    -- h(G.e) * h(G.e) * -h(G.e) =
    -- h(G.e * G.e) * -h(G.e) =
    -- h(G.e) * -h(G.e) =
    -- H.e
    theorem e_to_e : H.map 1 = 1 :=
    begin
      rw ← group.mul_e (H.map 1),
      rw ← group.mul_right_inv (H.map 1),
      rw ← group.mul_assoc,
      rw ← homomorphism.mul_holds,
      rw group.mul_e,
    end

    -- h(-x) =
    -- h(-x) * H.e =
    -- h(-x) * h(x) * -h(x) =
    -- h(-x * x) * -h(x) =
    -- h(G.e) * -h(x) =
    -- H.e * -h(x) =
    -- -h(x)
    theorem inv_to_inv (x : α) : H.map x⁻¹ = (H.map x)⁻¹ :=
    begin
      rw ← group.mul_e (H.map x⁻¹),
      rw ← group.mul_right_inv (H.map x),
      rw ← group.mul_assoc,
      rw ← homomorphism.mul_holds,
      rw group.mul_left_inv,
      rw homomorphism.e_to_e,
      rw group.e_mul,
    end

  end homomorphism

end hidden