feat(data/equiv/mul_add): monoids/rings with one element are isomorph…

…ic (#6079)

Monoids (resp. add_monoids, semirings) with one element are isomorphic.

src/data/equiv/mul_add.lean

@@ -15,6 +15,9 @@ datatypes representing isomorphisms of `add_monoid`s/`add_group`s and `monoid`s/
 
 ## Notations
 
+* ``infix ` ≃* `:25 := mul_equiv``
+* ``infix ` ≃+ `:25 := add_equiv``
+
 The extended equivs all have coercions to functions, and the coercions are the canonical
 notation when treating the isomorphisms as maps.
 
@@ -157,7 +160,48 @@ e.to_equiv.symm_apply_eq
 lemma eq_symm_apply (e : M ≃* N) {x y} : y = e.symm x ↔ e y = x :=
 e.to_equiv.eq_symm_apply
 
-/-- a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism) -/
+/-- Two multiplicative isomorphisms agree if they are defined by the
+    same underlying function. -/
+@[ext, to_additive
+  "Two additive isomorphisms agree if they are defined by the same underlying function."]
+lemma ext {f g : mul_equiv M N} (h : ∀ x, f x = g x) : f = g :=
+begin
+  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
+  cases f, cases g, congr,
+  { exact (funext h) },
+  { exact congr_arg equiv.inv_fun h₁ }
+end
+
+attribute [ext] add_equiv.ext
+
+@[to_additive]
+lemma ext_iff {f g : mul_equiv M N} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
+@[to_additive]
+protected lemma congr_arg {f : mul_equiv M N} : Π {x x' : M}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+@[to_additive]
+protected lemma congr_fun {f g : mul_equiv M N} (h : f = g) (x : M) : f x = g x := h ▸ rfl
+
+/-- The `mul_equiv` between two monoids with a unique element. -/
+@[to_additive "The `add_equiv` between two add_monoids with a unique element."]
+def mul_equiv_of_unique_of_unique {M N}
+  [unique M] [unique N] [has_mul M] [has_mul N] : M ≃* N :=
+{ map_mul' := λ _ _, subsingleton.elim _ _,
+  ..equiv_of_unique_of_unique }
+
+/-- There is a unique monoid homomorphism between two monoids with a unique element. -/
+@[to_additive] instance {M N} [unique M] [unique N] [has_mul M] [has_mul N] : unique (M ≃* N) :=
+{ default := mul_equiv_of_unique_of_unique ,
+  uniq := λ _, ext $ λ x, subsingleton.elim _ _}
+
+/-!
+## Monoids
+-/
+
+/-- A multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism). -/
 @[simp, to_additive]
 lemma map_one {M N} [monoid M] [monoid N] (h : M ≃* N) : h 1 = 1 :=
 by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←h.map_mul, one_mul]
@@ -198,39 +242,18 @@ lemma to_monoid_hom_apply {M N} [monoid M] [monoid N] (e : M ≃* N) (x : M) :
   e.to_monoid_hom x = e x :=
 rfl
 
-/-- A multiplicative equivalence of groups preserves inversion. -/
-@[simp, to_additive]
-lemma map_inv [group G] [group H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
-h.to_monoid_hom.map_inv x
-
-/-- Two multiplicative isomorphisms agree if they are defined by the
-    same underlying function. -/
-@[ext, to_additive
-  "Two additive isomorphisms agree if they are defined by the same underlying function."]
-lemma ext {f g : mul_equiv M N} (h : ∀ x, f x = g x) : f = g :=
-begin
-  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
-  cases f, cases g, congr,
-  { exact (funext h) },
-  { exact congr_arg equiv.inv_fun h₁ }
-end
-
-@[to_additive]
-protected lemma congr_arg {f : mul_equiv M N} : Π {x x' : M}, x = x' → f x = f x'
-| _ _ rfl := rfl
-
-@[to_additive]
-protected lemma congr_fun {f g : mul_equiv M N} (h : f = g) (x : M) : f x = g x := h ▸ rfl
-
-@[to_additive]
-lemma ext_iff {f g : mul_equiv M N} : f = g ↔ ∀ x, f x = g x :=
-⟨λ h x, h ▸ rfl, ext⟩
-
 @[to_additive] lemma to_monoid_hom_injective
   {M N} [monoid M] [monoid N] : function.injective (to_monoid_hom : (M ≃* N) → M →* N) :=
 λ f g h, mul_equiv.ext (monoid_hom.ext_iff.1 h)
 
-attribute [ext] add_equiv.ext
+/-!
+# Groups
+-/
+
+/-- A multiplicative equivalence of groups preserves inversion. -/
+@[simp, to_additive]
+lemma map_inv [group G] [group H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
+h.to_monoid_hom.map_inv x
 
 end mul_equiv
 

src/data/equiv/ring.lean

@@ -16,6 +16,8 @@ corresponding group of automorphisms `ring_aut`.
 
 ## Notations
 
+* ``infix ` ≃+* `:25 := ring_equiv``
+
 The extended equiv have coercions to functions, and the coercion is the canonical notation when
 treating the isomorphism as maps.
 
@@ -96,6 +98,17 @@ instance has_coe_to_add_equiv : has_coe (R ≃+* S) (R ≃+ S) := ⟨ring_equiv.
 @[norm_cast] lemma coe_add_equiv (f : R ≃+* S) (a : R) :
   (f : R ≃+ S) a = f a := rfl
 
+/-- The `ring_equiv` between two semirings with a unique element. -/
+def ring_equiv_of_unique_of_unique {M N}
+  [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] : M ≃+* N :=
+{ ..add_equiv.add_equiv_of_unique_of_unique,
+  ..mul_equiv.mul_equiv_of_unique_of_unique}
+
+instance {M N} [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] :
+  unique (M ≃+* N) :=
+{ default := ring_equiv_of_unique_of_unique,
+  uniq := λ _, ext $ λ x, subsingleton.elim _ _ }
+
 variable (R)
 
 /-- The identity map is a ring isomorphism. -/