feat(data/equiv/functor): bifunctor.map_equiv (#2241)

* feat(data/equiv/functor): bifunctor.map_equiv

* add documentation, and make the function an explicit argument

* Update src/data/equiv/functor.lean

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/equiv/functor.lean

@@ -1,20 +1,74 @@
 /-
 Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Simon Hudon
+Authors: Johan Commelin, Simon Hudon, Scott Morrison
 -/
 
 import data.equiv.basic
+import category.bifunctor
 
-universes u v
+/-!
+# Functor and bifunctors can be applied to `equiv`s.
 
-variables {α β : Type u} {f : Type u → Type v} [functor f] [is_lawful_functor f]
-open functor equiv function is_lawful_functor
+We define
+```lean
+def functor.map_equiv (f : Type u → Type v) [functor f] [is_lawful_functor f] :
+  α ≃ β → f α ≃ f β
+```
+and
+```lean
+def bifunctor.map_equiv (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] :
+  α ≃ β → α' ≃ β' → F α α' ≃ F β β'
+```
+-/
+
+universes u v w
+
+variables {α β : Type u}
+open equiv
+
+namespace functor
 
-def functor.map_equiv (h : α ≃ β) : f α ≃ f β :=
+variables (f : Type u → Type v) [functor f] [is_lawful_functor f]
+
+/-- Apply a functor to an `equiv`. -/
+def map_equiv (h : α ≃ β) : f α ≃ f β :=
 { to_fun    := map h,
   inv_fun   := map h.symm,
   left_inv  := λ x,
     by { rw map_map, convert is_lawful_functor.id_map x, ext a, apply symm_apply_apply },
   right_inv := λ x,
     by { rw map_map, convert is_lawful_functor.id_map x, ext a, apply apply_symm_apply } }
+
+@[simp]
+lemma map_equiv_apply (h : α ≃ β) (x : f α) :
+  (map_equiv f h : f α ≃ f β) x = map h x := rfl
+
+@[simp]
+lemma map_equiv_symm_apply (h : α ≃ β) (y : f β) :
+  (map_equiv f h : f α ≃ f β).symm y = map h.symm y := rfl
+
+end functor
+
+namespace bifunctor
+
+variables {α' β' : Type v} (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F]
+
+/-- Apply a bifunctor to a pair of `equiv`s. -/
+def map_equiv (h : α ≃ β) (h' : α' ≃ β') : F α α' ≃ F β β' :=
+{ to_fun    := bimap h h',
+  inv_fun   := bimap h.symm h'.symm,
+  left_inv  := λ x,
+    by { rw bimap_bimap, convert is_lawful_bifunctor.id_bimap x; { ext a, apply symm_apply_apply } },
+  right_inv := λ x,
+    by { rw bimap_bimap, convert is_lawful_bifunctor.id_bimap x; { ext a, apply apply_symm_apply } } }
+
+@[simp]
+lemma map_equiv_apply (h : α ≃ β) (h' : α' ≃ β') (x : F α α') :
+  (map_equiv F h h' : F α α' ≃ F β β') x = bimap h h' x := rfl
+
+@[simp]
+lemma map_equiv_symm_apply (h : α ≃ β) (h' : α' ≃ β') (y : F β β') :
+  (map_equiv F h h' : F α α' ≃ F β β').symm y = bimap h.symm h'.symm y := rfl
+
+end bifunctor

src/ring_theory/free_comm_ring.lean

@@ -279,7 +279,7 @@ end
 def subsingleton_equiv_free_comm_ring [subsingleton α] :
   free_ring α ≃+* free_comm_ring α :=
 @ring_equiv.of' (free_ring α) (free_comm_ring α) _ _
-  (@functor.map_equiv _ _ free_abelian_group _ _ $ multiset.subsingleton_equiv α) $
+  (functor.map_equiv free_abelian_group (multiset.subsingleton_equiv α)) $
   begin
     delta functor.map_equiv,
     rw congr_arg is_ring_hom _,