chore(group_theory/eckmann_hilton): use mul_one_class and is_(left|right)_id (#7370)

This ties these theorems slightly more to the rest of mathlib.

The changes are:

* `eckmann_hilton.comm_monoid` now promotes a `mul_one_class` to a `comm_monoid` rather than taking two `is_unital` objects. This makes it consistent with `eckmann_hilton.comm_group`.
* `is_unital` is no longer a `class`, since it never had any instances and was never used as a typeclass argument.
* `is_unital` is now defined in terms of `is_left_id` and `is_right_id`.
* `add_group.is_unital` has been renamed to `eckmann_hilton.add_zero_class.is_unital` - the missing namespace was an accident, and the definition works much more generally than it was originally stated for.

Author: eric-wieser

src/group_theory/eckmann_hilton.lean

@@ -14,8 +14,8 @@ The main application lies in proving that higher homotopy groups (`πₙ` for `n
 
 ## Main declarations
 
-* `eckmann_hilton.comm_monoid`: If a type carries two unital binary operations that distribute
-  over each other, then these operations are equal, and form a commutative monoid structure.
+* `eckmann_hilton.comm_monoid`: If a type carries a unital magma structure that distributes
+  over a unital binary operation, then the magma is a commutative monoid.
 * `eckmann_hilton.comm_group`: If a type carries a group structure that distributes
   over a unital binary operation, then the group is commutative.
 
@@ -31,12 +31,11 @@ local notation a `<`m`>` b := m a b
 
 /-- `is_unital m e` expresses that `e : X` is a left and right unit
 for the binary operation `m : X → X → X`. -/
-class is_unital (m : X → X → X) (e : X) : Prop :=
-(one_mul : ∀ x : X, (e <m> x) = x)
-(mul_one : ∀ x : X, (x <m> e) = x)
+structure is_unital (m : X → X → X) (e : X) extends is_left_id _ m e, is_right_id _ m e : Prop.
 
-@[to_additive add_group.is_unital]
-lemma group.is_unital [G : group X] : is_unital (*) (1 : X) := { ..G }
+@[to_additive eckmann_hilton.add_zero_class.is_unital]
+lemma mul_one_class.is_unital [G : mul_one_class X] : is_unital (*) (1 : X) :=
+is_unital.mk (by apply_instance) (by apply_instance)
 
 variables {m₁ m₂ : X → X → X} {e₁ e₂ : X}
 variables (h₁ : is_unital m₁ e₁) (h₂ : is_unital m₂ e₂)
@@ -49,55 +48,56 @@ then they have the same unit elements.
 In fact, the two operations are the same, and give a commutative monoid structure,
 see `eckmann_hilton.comm_monoid`. -/
 lemma one : e₁ = e₂ :=
-by simpa only [h₁.one_mul, h₁.mul_one, h₂.one_mul, h₂.mul_one] using distrib e₂ e₁ e₁ e₂
+by simpa only [h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂
 
 /-- If a type carries two unital binary operations that distribute over each other,
 then these operations are equal.
 
 In fact, they give a commutative monoid structure, see `eckmann_hilton.comm_monoid`. -/
-lemma mul : (m₁ = m₂) :=
+lemma mul : m₁ = m₂ :=
 begin
   funext a b,
   calc m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) :
-    by simp only [one h₁ h₂ distrib, h₁.one_mul, h₁.mul_one, h₂.one_mul, h₂.mul_one]
+    by simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
           ... = m₂ a b :
-    by simp only [distrib, h₁.one_mul, h₁.mul_one, h₂.one_mul, h₂.mul_one]
+    by simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
 end
 
 /-- If a type carries two unital binary operations that distribute over each other,
 then these operations are commutative.
 
 In fact, they give a commutative monoid structure, see `eckmann_hilton.comm_monoid`. -/
 lemma mul_comm : is_commutative _ m₂ :=
-⟨λ a b, by simpa [mul h₁ h₂ distrib, h₂.one_mul, h₂.mul_one] using distrib e₂ a b e₂⟩
+⟨λ a b, by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂⟩
 
 /-- If a type carries two unital binary operations that distribute over each other,
 then these operations are associative.
 
 In fact, they give a commutative monoid structure, see `eckmann_hilton.comm_monoid`. -/
 lemma mul_assoc : is_associative _ m₂ :=
-⟨λ a b c, by simpa [mul h₁ h₂ distrib, h₂.one_mul, h₂.mul_one] using distrib a b e₂ c⟩
-
-/-- If a type carries two unital binary operations that distribute over each other,
-then these operations are equal, and form a commutative monoid structure. -/
-@[to_additive "If a type carries two unital binary operations that distribute over each other,
-then these operations are equal, and form a additive commutative monoid structure."]
-def comm_monoid : comm_monoid X :=
-{ mul := m₂,
-  one := e₂,
-  mul_comm := (mul_comm h₁ h₂ distrib).comm,
-  mul_assoc := (mul_assoc h₁ h₂ distrib).assoc,
-  ..h₂ }
+⟨λ a b c, by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c⟩
 
 omit h₁ h₂ distrib
 
+/-- If a type carries a unital magma structure that distributes over a unital binary
+operations, then the magma structure is a commutative monoid. -/
+@[to_additive "If a type carries a unital additive magma structure that distributes over a
+unital binary operations, then the additive magma structure is a commutative additive monoid."]
+def comm_monoid [h : mul_one_class X]
+  (distrib : ∀ a b c d, ((a * b) <m₁> (c * d)) = ((a <m₁> c) * (b <m₁> d))) : comm_monoid X :=
+{ mul := (*),
+  one := 1,
+  mul_comm := (mul_comm h₁ mul_one_class.is_unital distrib).comm,
+  mul_assoc := (mul_assoc h₁ mul_one_class.is_unital distrib).assoc,
+  ..h }
+
 /-- If a type carries a group structure that distributes over a unital binary operation,
 then the group is commutative. -/
 @[to_additive "If a type carries an additive group structure that distributes
 over a unital binary operation, then the additive group is commutative."]
 def comm_group [G : group X]
   (distrib : ∀ a b c d, ((a * b) <m₁> (c * d)) = ((a <m₁> c) * (b <m₁> d))) : comm_group X :=
-{ mul_comm := (eckmann_hilton.comm_monoid h₁ group.is_unital distrib).mul_comm,
+{ ..(eckmann_hilton.comm_monoid h₁ distrib),
   ..G }
 
 end eckmann_hilton