Alternative axioms of a group in LEAN

group.lean

-- The First-order theory of groups

constant G : Type -- the group
constant m : G × G → G -- the multiplication symbol

notation a `*` b := m (a, b)

-- the group axioms
axiom non_empty : ∃ (g : G), true
axiom mul_assoc : ∀ (a b c : G), m (m (a, b), c) = m (a, m (b, c))
axiom left_path : ∀ (a b : G), ∃ (c : G), m (c, a) = b
axiom right_path : ∀ (a b : G), ∃ (d : G), m (a, d) = b

-- showing that these axioms imply the regular ones

/-A left identity of one element is also a left identity of any another element-/
lemma same_left_id (a b c : G) (c_left_a_a : m (c, a) = a) : m (c, b) = b := 
begin
  cases right_path a b with d d_right_a_b,
  rw [← d_right_a_b, ← mul_assoc, c_left_a_a],
end

/-A restatement of the previous lemma. If `c` is a left identity of `a`, it is the left identity of every other element-/
lemma universal_left_id (a c : G) (c_left_a_a : m (c, a) = a) : ∀ (b : G), m (c, b) = b :=
begin
  intro b,
  exact same_left_id a b c c_left_a_a,
end

/-A right identity of one element is also a right identity of any another element-/
lemma same_right_id (a b d : G) (d_right_a_a : m (a, d) = a) : m (b, d) = b :=
begin
  cases left_path a b with c c_left_a_b,
  rw [← c_left_a_b, mul_assoc, d_right_a_a],
end

/-A restatement of the previous lemma. If `c` is a right identity of `a`, it is the right identity of every other element-/
lemma universal_right_id (a d : G) (d_right_a_a : m (a, d) = a) : ∀ (b : G), m (b, d) = b :=
begin
  intro b,
  exact same_right_id a b d d_right_a_a,
end

/-If `eₗ` is a universal left identity element and `eᵣ` is a universal right identity element, then `eₗ = eᵣ`.-/
lemma univ_left_id_eq_univ_right_id (eₗ eᵣ : G) (eₗ_left_id : ∀ (a : G), m (eₗ, a) = a) (eᵣ_right_id : ∀ (a : G), m ( a, eᵣ) = a) : eₗ = eᵣ :=
begin
  have h_eₗ : m (eₗ, eᵣ) = eₗ := eᵣ_right_id eₗ,
  have h_eᵣ : m (eₗ, eᵣ) = eᵣ := eₗ_left_id eᵣ,
  exact eq.trans (eq.symm h_eₗ) h_eᵣ,
end

/-If `e` is a left identity of `a`, it is also a right identity of `a`. This is slightly different from the previous lemma.-/
lemma left_id_eq_right_id (a e : G) (e_left_a_a : m (e, a) = a) : (m (a, e) = a) := 
begin
  have e_right_e_e : m (e, e) = e := (universal_left_id a e e_left_a_a) e,
  exact (universal_right_id e e e_right_e_e) a,
end

/-This is almost exactly the same as the previous lemma. It is introduced only to make the names symmetric.-/
lemma right_id_eq_left_id (a e : G) (e_right_a_a : m (a, e) = a) : (m (e, a) = a) :=
begin
  have e_left_a_a : m (e, e) = e := (universal_right_id a e e_right_a_a) e,
  exact (universal_left_id e e e_left_a_a) a,
end

/-This is sufficiently important to deserve the theorem status. It states the existence of an identity element of the group-/
theorem universal_identity : ∃ (e : G), (∀ (a : G), m (e, a) = a) ∧ (∀ (a : G), m (a, e) = a) :=
begin
  cases non_empty with g t, --aside: this is the only place where the non-empty hypothesis is needed
  cases (left_path g g) with e e_left_g_g,
  have h_univ_left_id : ∀ (a: G), m (e, a) = a := universal_left_id g e e_left_g_g,
  have h_univ_right_id : ∀ (a : G), m (a, e) = a := universal_right_id g e (left_id_eq_right_id g e e_left_g_g),
  exact exists.intro e (and.intro h_univ_left_id h_univ_right_id),
end

/-This says that the idenitty element is unique. The proof is fairly standard-/
theorem unique_identity (e f : G) (id_e : (∀ (a : G), m (e, a) = a) ∧ (∀ (a : G), m (a, e) = a)) (id_f : (∀ (a : G), m (f, a) = a) ∧ (∀ (a : G), m (a, f) = a)) : e = f := 
begin
  exact univ_left_id_eq_univ_right_id e f id_e.1 id_f.2,
end

/-This states the existence of inverses, assuming the existence of some element `e` satisfying the criterion of an identity element-/
theorem group_inverses (e : G) (id_e : (∀ (a : G), m (e, a) = a) ∧ (∀ (a : G), m (a, e) = a)) : ∀ (a : G), ∃ (b : G), m (a, b) = e ∧ m (b, a) = e :=
begin
  intro a,
  cases (left_path a e) with b b_left_a_e,
  have b_right_a_e : m (a, b) = e :=
  begin
    cases (right_path a e) with c c_right_a_e,
    have c_eq_b : c = b :=
    begin
      have hb : m (b, e) = b := (id_e.2 b),
      have hc : m (b, e) = c := by rw [← c_right_a_e, ← mul_assoc, b_left_a_e, id_e.1 c],
      exact eq.symm (eq.trans (eq.symm hb) hc),
    end,
    rewrite c_eq_b at c_right_a_e,
    exact c_right_a_e,
  end,
  exact exists.intro b ⟨b_right_a_e, b_left_a_e⟩,
end

/-This combines the previous two theorems into one final theorem. This is needed as `group_inverses` was derived under the assumption that a certain `e` exists.-/
theorem group_axioms : ∃ (e : G), ( ( ∀ (a : G), m (e, a) = a) ∧ (∀ (a : G), m (a, e) = a) ) ∧ (∀ (a : G), ∃ (b : G), m (a, b) = e ∧ m (b, a) = e) :=
begin
  cases universal_identity with e h_id,
  
  have id_axioms : (( ∀ (a : G), m (e, a) = a) ∧ (∀ (a : G), m (a, e) = a) ) ∧ (∀ (a : G), ∃ (b : G), m (a, b) = e ∧ m (b, a) = e) :=
  begin
    split,
    exact h_id,
    exact group_inverses e h_id,
  end,
  
  exact exists.intro e id_axioms,
end

-- This shows that the usual axioms of a group can be derived from the above axioms. These axioms can be easily shown to be consequences of the usual ones.

---