feat(data/equiv,category_theory): prove equivalences are the same as …

…isos (leanprover-community#1587)

* refactor(category_theory,algebra/category): make algebraic categories not [reducible]

Adapted from part of leanprover-community#1438.

* Update src/algebra/category/CommRing/basic.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* adding missing forget2 instances

* Converting Reid's comment to a [Note]

* adding examples testing coercions

* feat(data/equiv/algebra): equivalence of algebraic equivalences and categorical isomorphisms

* more @[simps]

* more @[simps]

src/algebra/category/CommRing/basic.lean

@@ -132,3 +132,54 @@ instance has_forget_to_CommSemiRing : has_forget₂ CommRing CommSemiRing :=
 has_forget₂.mk' (λ R : CommRing, CommSemiRing.of R) (λ R, rfl) (λ R₁ R₂ f, f) (by tidy)
 
 end CommRing
+
+
+namespace ring_equiv
+
+variables {X Y : Type u}
+
+/-- Build an isomorphism in the category `Ring` from a `ring_equiv` between `ring`s. -/
+@[simps] def to_Ring_iso [ring X] [ring Y] (e : X ≃+* Y) : Ring.of X ≅ Ring.of Y :=
+{ hom := e.to_ring_hom,
+  inv := e.symm.to_ring_hom }
+
+/-- Build an isomorphism in the category `CommRing` from a `ring_equiv` between `comm_ring`s. -/
+@[simps] def to_CommRing_iso [comm_ring X] [comm_ring Y] (e : X ≃+* Y) : CommRing.of X ≅ CommRing.of Y :=
+{ hom := e.to_ring_hom,
+  inv := e.symm.to_ring_hom }
+
+end ring_equiv
+
+namespace category_theory.iso
+
+/-- Build a `ring_equiv` from an isomorphism in the category `Ring`. -/
+def Ring_iso_to_ring_equiv {X Y : Ring.{u}} (i : X ≅ Y) : X ≃+* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_add'  := by tidy,
+  map_mul'  := by tidy }.
+
+/-- Build a `ring_equiv` from an isomorphism in the category `CommRing`. -/
+def CommRing_iso_to_ring_equiv {X Y : CommRing.{u}} (i : X ≅ Y) : X ≃+* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_add'  := by tidy,
+  map_mul'  := by tidy }.
+
+end category_theory.iso
+
+/-- ring equivalences between `ring`s are the same as (isomorphic to) isomorphisms in `Ring`. -/
+def ring_equiv_iso_Ring_iso {X Y : Type u} [ring X] [ring Y] :
+  (X ≃+* Y) ≅ (Ring.of X ≅ Ring.of Y) :=
+{ hom := λ e, e.to_Ring_iso,
+  inv := λ i, i.Ring_iso_to_ring_equiv, }
+
+/-- ring equivalences between `comm_ring`s are the same as (isomorphic to) isomorphisms in `CommRing`. -/
+def ring_equiv_iso_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] :
+  (X ≃+* Y) ≅ (CommRing.of X ≅ CommRing.of Y) :=
+{ hom := λ e, e.to_CommRing_iso,
+  inv := λ i, i.CommRing_iso_to_ring_equiv, }

src/algebra/category/Group.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin
 
 import algebra.punit_instances
 import algebra.category.Mon.basic
+import category_theory.endomorphism
 
 /-!
 # Category instances for group, add_group, comm_group, and add_comm_group.
@@ -84,3 +85,75 @@ instance has_forget_to_CommMon : has_forget₂ CommGroup CommMon :=
 induced_category.has_forget₂ (λ G : CommGroup, CommMon.of G)
 
 end CommGroup
+
+
+variables {X Y : Type u}
+
+/-- Build an isomorphism in the category `Group` from a `mul_equiv` between `group`s. -/
+@[to_additive add_equiv.to_AddGroup_iso "Build an isomorphism in the category `AddGroup` from a `add_equiv` between `add_group`s."]
+def mul_equiv.to_Group_iso [group X] [group Y] (e : X ≃* Y) : Group.of X ≅ Group.of Y :=
+{ hom := e.to_monoid_hom,
+  inv := e.symm.to_monoid_hom }
+
+attribute [simps] mul_equiv.to_Group_iso add_equiv.to_AddGroup_iso
+
+/-- Build an isomorphism in the category `CommGroup` from a `mul_equiv` between `comm_group`s. -/
+@[simps, to_additive add_equiv.to_AddCommGroup_iso "Build an isomorphism in the category `AddCommGroup` from a `add_equiv` between `add_comm_group`s."]
+def mul_equiv.to_CommGroup_iso [comm_group X] [comm_group Y] (e : X ≃* Y) : CommGroup.of X ≅ CommGroup.of Y :=
+{ hom := e.to_monoid_hom,
+  inv := e.symm.to_monoid_hom }
+
+attribute [simps] mul_equiv.to_CommGroup_iso add_equiv.to_AddCommGroup_iso
+
+namespace category_theory.iso
+
+/-- Build a `mul_equiv` from an isomorphism in the category `Group`. -/
+@[to_additive AddGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category `AddGroup`."]
+def Group_iso_to_mul_equiv {X Y : Group.{u}} (i : X ≅ Y) : X ≃* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_mul'  := by tidy }.
+
+attribute [simps] Group_iso_to_mul_equiv AddGroup_iso_to_add_equiv
+
+/-- Build a `mul_equiv` from an isomorphism in the category `CommGroup`. -/
+@[to_additive AddCommGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category `AddCommGroup`."]
+def CommGroup_iso_to_mul_equiv {X Y : CommGroup.{u}} (i : X ≅ Y) : X ≃* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_mul'  := by tidy }.
+
+attribute [simps] CommGroup_iso_to_mul_equiv AddCommGroup_iso_to_add_equiv
+
+end category_theory.iso
+
+/-- multiplicative equivalences between `group`s are the same as (isomorphic to) isomorphisms in `Group` -/
+@[to_additive add_equiv_iso_AddGroup_iso "additive equivalences between `add_group`s are the same as (isomorphic to) isomorphisms in `AddGroup`"]
+def mul_equiv_iso_Group_iso {X Y : Type u} [group X] [group Y] :
+  (X ≃* Y) ≅ (Group.of X ≅ Group.of Y) :=
+{ hom := λ e, e.to_Group_iso,
+  inv := λ i, i.Group_iso_to_mul_equiv, }
+
+/-- multiplicative equivalences between `comm_group`s are the same as (isomorphic to) isomorphisms in `CommGroup` -/
+@[to_additive add_equiv_iso_AddCommGroup_iso "additive equivalences between `add_comm_group`s are the same as (isomorphic to) isomorphisms in `AddCommGroup`"]
+def mul_equiv_iso_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] :
+  (X ≃* Y) ≅ (CommGroup.of X ≅ CommGroup.of Y) :=
+{ hom := λ e, e.to_CommGroup_iso,
+  inv := λ i, i.CommGroup_iso_to_mul_equiv, }
+
+namespace category_theory.Aut
+
+/-- The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations. -/
+def iso_perm {α : Type u} : Group.of (Aut α) ≅ Group.of (equiv.perm α) :=
+{ hom := ⟨λ g, g.to_equiv, (by tidy), (by tidy)⟩,
+  inv := ⟨λ g, g.to_iso, (by tidy), (by tidy)⟩ }
+
+/-- The (unbundled) group of automorphisms of a type is `mul_equiv` to the (unbundled) group of permutations. -/
+def mul_equiv_perm {α : Type u} : Aut α ≃* equiv.perm α :=
+iso_perm.Group_iso_to_mul_equiv
+
+end category_theory.Aut

src/algebra/category/Mon/basic.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 
 import category_theory.concrete_category
 import algebra.group
+import data.equiv.algebra
 
 /-!
 # Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.
@@ -100,3 +101,72 @@ end CommMon
 -- We verify that the coercions of morphisms to functions work correctly:
 example {R S : Mon}     (f : R ⟶ S) : (R : Type) → (S : Type) := f
 example {R S : CommMon} (f : R ⟶ S) : (R : Type) → (S : Type) := f
+
+
+variables {X Y : Type u}
+
+section
+variables [monoid X] [monoid Y]
+
+/-- Build an isomorphism in the category `Mon` from a `mul_equiv` between `monoid`s. -/
+@[to_additive add_equiv.to_AddMon_iso "Build an isomorphism in the category `AddMon` from a `add_equiv` between `add_monoid`s."]
+def mul_equiv.to_Mon_iso (e : X ≃* Y) : Mon.of X ≅ Mon.of Y :=
+{ hom := e.to_monoid_hom,
+  inv := e.symm.to_monoid_hom }
+
+@[simp, to_additive add_equiv.to_AddMon_iso_hom]
+lemma mul_equiv.to_Mon_iso_hom {e : X ≃* Y} : e.to_Mon_iso.hom = e.to_monoid_hom := rfl
+@[simp, to_additive add_equiv.to_AddMon_iso_inv]
+lemma mul_equiv.to_Mon_iso_inv {e : X ≃* Y} : e.to_Mon_iso.inv = e.symm.to_monoid_hom := rfl
+end
+
+section
+variables [comm_monoid X] [comm_monoid Y]
+
+/-- Build an isomorphism in the category `CommMon` from a `mul_equiv` between `comm_monoid`s. -/
+@[to_additive add_equiv.to_AddCommMon_iso "Build an isomorphism in the category `AddCommMon` from a `add_equiv` between `add_comm_monoid`s."]
+def mul_equiv.to_CommMon_iso (e : X ≃* Y) : CommMon.of X ≅ CommMon.of Y :=
+{ hom := e.to_monoid_hom,
+  inv := e.symm.to_monoid_hom }
+
+@[simp, to_additive add_equiv.to_AddCommMon_iso_hom]
+lemma mul_equiv.to_CommMon_iso_hom {e : X ≃* Y} : e.to_CommMon_iso.hom = e.to_monoid_hom := rfl
+@[simp, to_additive add_equiv.to_AddCommMon_iso_inv]
+lemma mul_equiv.to_CommMon_iso_inv {e : X ≃* Y} : e.to_CommMon_iso.inv = e.symm.to_monoid_hom := rfl
+end
+
+namespace category_theory.iso
+
+/-- Build a `mul_equiv` from an isomorphism in the category `Mon`. -/
+@[to_additive AddMond_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category `AddMon`."]
+def Mon_iso_to_mul_equiv {X Y : Mon.{u}} (i : X ≅ Y) : X ≃* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_mul'  := by tidy }.
+
+/-- Build a `mul_equiv` from an isomorphism in the category `CommMon`. -/
+@[to_additive AddCommMon_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category `AddCommMon`."]
+def CommMon_iso_to_mul_equiv {X Y : CommMon.{u}} (i : X ≅ Y) : X ≃* Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  map_mul'  := by tidy }.
+
+end category_theory.iso
+
+/-- multiplicative equivalences between `monoid`s are the same as (isomorphic to) isomorphisms in `Mon` -/
+@[to_additive add_equiv_iso_AddMon_iso "additive equivalences between `add_monoid`s are the same as (isomorphic to) isomorphisms in `AddMon`"]
+def mul_equiv_iso_Mon_iso {X Y : Type u} [monoid X] [monoid Y] :
+  (X ≃* Y) ≅ (Mon.of X ≅ Mon.of Y) :=
+{ hom := λ e, e.to_Mon_iso,
+  inv := λ i, i.Mon_iso_to_mul_equiv, }
+
+/-- multiplicative equivalences between `comm_monoid`s are the same as (isomorphic to) isomorphisms in `CommMon` -/
+@[to_additive add_equiv_iso_AddCommMon_iso "additive equivalences between `add_comm_monoid`s are the same as (isomorphic to) isomorphisms in `AddCommMon`"]
+def mul_equiv_iso_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] :
+  (X ≃* Y) ≅ (CommMon.of X ≅ CommMon.of Y) :=
+{ hom := λ e, e.to_CommMon_iso,
+  inv := λ i, i.CommMon_iso_to_mul_equiv, }

src/algebra/group/to_additive.lean

@@ -162,7 +162,7 @@ do
 
 meta def proceed_fields (env : environment) (src tgt : name) (prio : ℕ) : command :=
 let aux := proceed_fields_aux src tgt prio in
-do 
+do
 aux (λ n, pure $ list.map name.to_string $ (env.structure_fields n).get_or_else []) >>
 aux (λ n, (list.map (λ (x : name), "to_" ++ x.to_string) <$>
                             (ancestor_attr.get_param n <|> pure []))) >>

src/category_theory/concrete_category/basic.lean

@@ -84,6 +84,13 @@ congr_fun ((forget _).map_id X) x
   (f ≫ g) x = g (f x) :=
 congr_fun ((forget _).map_comp _ _) x
 
+@[simp] lemma coe_hom_inv_id {X Y : C} (f : X ≅ Y) (x : X) :
+  f.inv (f.hom x) = x :=
+congr_fun ((forget C).map_iso f).hom_inv_id x
+@[simp] lemma coe_inv_hom_id {X Y : C} (f : X ≅ Y) (y : Y) :
+  f.hom (f.inv y) = y :=
+congr_fun ((forget C).map_iso f).inv_hom_id y
+
 end
 
 instance concrete_category.types : concrete_category (Type u) :=

src/category_theory/conj.lean

@@ -91,9 +91,9 @@ is_monoid_hom.map_pow α.conj f n
 
 /-- `conj` defines a group isomorphisms between groups of automorphisms -/
 def conj_Aut : Aut X ≃* Aut Y :=
-(Aut.units_End_eqv_Aut X).symm.trans $
+(Aut.units_End_equiv_Aut X).symm.trans $
 (units.map_equiv α.conj).trans $
-Aut.units_End_eqv_Aut Y
+Aut.units_End_equiv_Aut Y
 
 lemma conj_Aut_apply (f : Aut X) : α.conj_Aut f = α.symm ≪≫ f ≪≫ α :=
 by cases f; cases α; ext; refl

src/category_theory/endomorphism.lean

@@ -58,12 +58,16 @@ attribute [ext Aut] iso.ext
 
 namespace Aut
 
-instance: group (Aut X) :=
+instance : group (Aut X) :=
 by refine { one := iso.refl X,
             inv := iso.symm,
             mul := flip iso.trans, .. } ; dunfold flip; obviously
 
-def units_End_eqv_Aut : units (End X) ≃* Aut X :=
+/--
+Units in the monoid of endomorphisms of an object
+are (multiplicatively) equivalent to automorphisms of that object.
+-/
+def units_End_equiv_Aut : units (End X) ≃* Aut X :=
 { to_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
   inv_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
   left_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,

src/category_theory/single_obj.lean

@@ -124,9 +124,12 @@ namespace units
 
 variables (α : Type u) [monoid α]
 
+/--
+The units in a monoid are (multiplicatively) equivalent to
+the automorphisms of `star` when we think of the monoid as a single-object category. -/
 def to_Aut : units α ≃* Aut (single_obj.star α) :=
 (units.map_equiv (single_obj.to_End α)).trans $
-  Aut.units_End_eqv_Aut _
+  Aut.units_End_equiv_Aut _
 
 @[simp] lemma to_Aut_hom (x : units α) : (to_Aut α x).hom = single_obj.to_End α x := rfl
 @[simp] lemma to_Aut_inv (x : units α) :

src/category_theory/types.lean

@@ -170,3 +170,22 @@ def to_equiv (i : X ≅ Y) : X ≃ Y :=
 @[simp] lemma to_equiv_symm_fun (i : X ≅ Y) : (i.to_equiv.symm : Y → X) = i.inv := rfl
 
 end category_theory.iso
+
+
+universe u
+
+-- We prove `equiv_iso_iso` and then use that to sneakily construct `equiv_equiv_iso`.
+-- (In this order the proofs are handled by `obviously`.)
+
+/-- equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types -/
+@[simps] def equiv_iso_iso {X Y : Type u} : (X ≃ Y) ≅ (X ≅ Y) :=
+{ hom := λ e, e.to_iso,
+  inv := λ i, i.to_equiv, }
+
+/-- equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types -/
+-- We leave `X` and `Y` as explicit arguments here, because the coercions from `equiv` to a function won't fire without them.
+def equiv_equiv_iso (X Y : Type u) : (X ≃ Y) ≃ (X ≅ Y) :=
+(equiv_iso_iso).to_equiv
+
+@[simp] lemma equiv_equiv_iso_hom {X Y : Type u} (e : X ≃ Y) : (equiv_equiv_iso X Y) e = e.to_iso := rfl
+@[simp] lemma equiv_equiv_iso_inv {X Y : Type u} (e : X ≅ Y) : (equiv_equiv_iso X Y).symm e = e.to_equiv := rfl

src/data/equiv/algebra.lean

@@ -304,13 +304,26 @@ lemma map_ne_one_iff {α β} [monoid α] [monoid β] (h : α ≃* β) (x : α) :
   h x ≠ 1 ↔ x ≠ 1 :=
 ⟨mt (h.map_eq_one_iff x).2, mt (h.map_eq_one_iff x).1⟩
 
-/-- A multiplicative bijection between two monoids is an isomorphism. -/
+/--
+Extract the forward direction of a multiplicative equivalence
+as a multiplication preserving function.
+-/
 @[to_additive to_add_monoid_hom]
 def to_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : (α →* β) :=
 { to_fun := h,
   map_mul' := h.map_mul,
   map_one' := h.map_one }
 
+@[simp, to_additive]
+lemma to_monoid_hom_apply_symm_to_monoid_hom_apply {α β} [monoid α] [monoid β] (e : α ≃* β) :
+  ∀ (y : β), e.to_monoid_hom (e.symm.to_monoid_hom y) = y :=
+e.to_equiv.apply_symm_apply
+
+@[simp, to_additive]
+lemma symm_to_monoid_hom_apply_to_monoid_hom_apply {α β} [monoid α] [monoid β] (e : α ≃* β) :
+  ∀ (x : α), e.symm.to_monoid_hom (e.to_monoid_hom x) = x :=
+equiv.symm_apply_apply (e.to_equiv)
+
 /-- A multiplicative equivalence of groups preserves inversion. -/
 @[to_additive]
 lemma map_inv {α β} [group α] [group β] (h : α ≃* β) (x : α) : h x⁻¹ = (h x)⁻¹ :=
@@ -511,6 +524,16 @@ def of (e : α ≃ β) [is_semiring_hom e] : α ≃+* β :=
 
 instance (e : α ≃+* β) : is_semiring_hom e := e.to_ring_hom.is_semiring_hom
 
+@[simp]
+lemma to_ring_hom_apply_symm_to_ring_hom_apply {α β} [semiring α] [semiring β] (e : α ≃+* β) :
+  ∀ (y : β), e.to_ring_hom (e.symm.to_ring_hom y) = y :=
+e.to_equiv.apply_symm_apply
+
+@[simp]
+lemma symm_to_ring_hom_apply_to_ring_hom_apply {α β} [semiring α] [semiring β] (e : α ≃+* β) :
+  ∀ (x : α), e.symm.to_ring_hom (e.to_ring_hom x) = x :=
+equiv.symm_apply_apply (e.to_equiv)
+
 end semiring_hom
 
 section ring_hom