feat(category_theory/cones): map_cone_inv as an equivalence (#4253)

When `G` is an equivalence, we have `G.map_cone_inv : cone (F ⋙ G) → cone F`, and that this is an inverse to `G.map_cone`, but not quite that these constitute an equivalence of categories. This PR fixes that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/category_theory/equivalence.lean

@@ -66,11 +66,11 @@ begin
   exact e.functor_unit_comp X
 end
 
-lemma functor_unit (e : C ≌ D) (X : C) :
-  e.functor.map (e.unit.app X) = e.counit_inv.app (e.functor.obj X) :=
-by { erw [←iso.comp_hom_eq_id (e.counit_iso.app _), functor_unit_comp], refl }
+lemma counit_inv_app_functor (e : C ≌ D) (X : C) :
+  e.counit_inv.app (e.functor.obj X) = e.functor.map (e.unit.app X) :=
+by { symmetry, erw [←iso.comp_hom_eq_id (e.counit_iso.app _), functor_unit_comp], refl }
 
-lemma counit_functor (e : C ≌ D) (X : C) :
+lemma counit_app_functor (e : C ≌ D) (X : C) :
   e.counit.app (e.functor.obj X) = e.functor.map (e.unit_inv.app X) :=
 by { erw [←iso.hom_comp_eq_id (e.functor.map_iso (e.unit_iso.app X)), functor_unit_comp], refl }
 
@@ -105,13 +105,13 @@ begin
   exact e.unit_inverse_comp Y
 end
 
-lemma unit_inverse (e : C ≌ D) (Y : D) :
+lemma unit_app_inverse (e : C ≌ D) (Y : D) :
   e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counit_inv.app Y) :=
 by { erw [←iso.comp_hom_eq_id (e.inverse.map_iso (e.counit_iso.app Y)), unit_inverse_comp], refl }
 
-lemma inverse_counit (e : C ≌ D) (Y : D) :
-  e.inverse.map (e.counit.app Y) = e.unit_inv.app (e.inverse.obj Y) :=
-by { erw [←iso.hom_comp_eq_id (e.unit_iso.app _), unit_inverse_comp], refl }
+lemma unit_inv_app_inverse (e : C ≌ D) (Y : D) :
+  e.unit_inv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) :=
+by { symmetry, erw [←iso.hom_comp_eq_id (e.unit_iso.app _), unit_inverse_comp], refl }
 
 @[simp] lemma fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
   e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counit_inv.app Y :=
@@ -178,8 +178,8 @@ variables {E : Type u₃} [category.{v₃} E]
   functor_unit_iso_comp' := λ X,
   begin
     dsimp,
-    rw [← f.functor.map_comp_assoc, e.functor.map_comp, functor_unit, fun_inv_map,
-        iso.inv_hom_id_app_assoc, assoc, iso.inv_hom_id_app, counit_functor, ← functor.map_comp],
+    rw [← f.functor.map_comp_assoc, e.functor.map_comp, ←counit_inv_app_functor, fun_inv_map,
+        iso.inv_hom_id_app_assoc, assoc, iso.inv_hom_id_app, counit_app_functor, ← functor.map_comp],
     erw [comp_id, iso.hom_inv_id_app, functor.map_id],
   end }
 

src/category_theory/limits/cones.lean

@@ -251,7 +251,7 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
     intro k,
     have t := s.π.naturality (e.unit_inv.app k),
     dsimp at t,
-    simp only [←e.counit_functor k, id_comp] at t,
+    simp only [←e.counit_app_functor k, id_comp] at t,
     dsimp,
     simp [t],
   end)) (by tidy), }
@@ -281,6 +281,7 @@ def forget : cone F ⥤ C :=
 
 variables {D : Type u'} [category.{v} D] (G : C ⥤ D)
 
+/-- A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially. -/
 @[simps] def functoriality : cone F ⥤ cone (F ⋙ G) :=
 { obj := λ A,
   { X := G.obj A.X,
@@ -297,6 +298,20 @@ instance functoriality_full [full G] [faithful G] : full (functoriality F G) :=
 instance functoriality_faithful [faithful G] : faithful (cones.functoriality F G) :=
 { map_injective' := λ X Y f g e, by { ext1, injection e, apply G.map_injective h_1 } }
 
+/--
+If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
+equivalence between cones over `F` and cones over `F ⋙ e.functor`.
+-/
+@[simps]
+def functoriality_equivalence (e : C ≌ D) : cone F ≌ cone (F ⋙ e.functor) :=
+let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F :=
+  functor.associator _ _ _ ≪≫ iso_whisker_left _ (e.unit_iso).symm ≪≫ functor.right_unitor _ in
+{ functor := functoriality F e.functor,
+  inverse := (functoriality (F ⋙ e.functor) e.inverse) ⋙
+    (postcompose_equivalence f).functor,
+  unit_iso := nat_iso.of_components (λ c, cones.ext (e.unit_iso.app _) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ c, cones.ext (e.counit_iso.app _) (by tidy)) (by tidy), }
+
 /--
 If `F` reflects isomorphisms, then `cones.functoriality F` reflects isomorphisms
 as well.
@@ -400,7 +415,7 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
     intro k,
     have t := s.ι.naturality (e.unit.app k),
     dsimp at t,
-    simp only [e.functor_unit k, comp_id] at t,
+    simp only [←e.counit_inv_app_functor k, comp_id] at t,
     dsimp,
     simp [t],
   end)) (by tidy), }
@@ -430,6 +445,7 @@ def forget : cocone F ⥤ C :=
 
 variables {D : Type u'} [category.{v} D] (G : C ⥤ D)
 
+/-- A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially. -/
 @[simps] def functoriality : cocone F ⥤ cocone (F ⋙ G) :=
 { obj := λ A,
   { X := G.obj A.X,
@@ -446,6 +462,29 @@ instance functoriality_full [full G] [faithful G] : full (functoriality F G) :=
 instance functoriality_faithful [faithful G] : faithful (functoriality F G) :=
 { map_injective' := λ X Y f g e, by { ext1, injection e, apply G.map_injective h_1 } }
 
+/--
+If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
+equivalence between cocones over `F` and cocones over `F ⋙ e.functor`.
+-/
+@[simps]
+def functoriality_equivalence (e : C ≌ D) : cocone F ≌ cocone (F ⋙ e.functor) :=
+let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F :=
+  functor.associator _ _ _ ≪≫ iso_whisker_left _ (e.unit_iso).symm ≪≫ functor.right_unitor _ in
+{ functor := functoriality F e.functor,
+  inverse := (functoriality (F ⋙ e.functor) e.inverse) ⋙
+    (precompose_equivalence f.symm).functor,
+  unit_iso := nat_iso.of_components (λ c, cocones.ext (e.unit_iso.app _) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ c, cocones.ext (e.counit_iso.app _)
+  begin
+    -- Unfortunately this doesn't work by `tidy`.
+    -- In this configuration `simp` reaches a dead-end and needs help.
+    intros j,
+    dsimp,
+    simp only [←equivalence.counit_inv_app_functor, iso.inv_hom_id_app, map_comp, equivalence.fun_inv_map,
+      assoc, id_comp, iso.inv_hom_id_app_assoc],
+    dsimp, simp, -- See note [dsimp, simp].
+  end) (by tidy), }
+
 /--
 If `F` reflects isomorphisms, then `cocones.functoriality F` reflects isomorphisms
 as well.
@@ -480,17 +519,6 @@ def map_cocone (c : cocone F) : cocone (F ⋙ H) := (cocones.functoriality F H).
 @[simp] lemma map_cone_X (c : cone F) : (H.map_cone c).X = H.obj c.X := rfl
 @[simp] lemma map_cocone_X (c : cocone F) : (H.map_cocone c).X = H.obj c.X := rfl
 
-/-- If `H` is an equivalence, we invert `H.map_cone` and get an original cone for `F` from a cone
-for `F ⋙ H`.-/
-@[simps]
-def map_cone_inv [is_equivalence H]
-  (c : cone (F ⋙ H)) : cone F :=
-let t := (inv H).map_cone c in
-let α : (F ⋙ H) ⋙ inv H ⟶ F :=
-  ((whisker_left F H.fun_inv_id.hom) : F ⋙ (H ⋙ inv H) ⟶ _) ≫ (functor.right_unitor _).hom in
-{ X := t.X,
-  π := ((category_theory.cones J C).map α).app (op t.X) t.π }
-
 /-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially.  -/
 def map_cone_morphism   {c c' : cone F}   (f : c ⟶ c')   :
   H.map_cone c ⟶ H.map_cone c' := (cones.functoriality F H).map f
@@ -503,22 +531,37 @@ def map_cocone_morphism {c c' : cocone F} (f : c ⟶ c') :
 @[simp] lemma map_cocone_ι (c : cocone F) (j : J) :
   (map_cocone H c).ι.app j = H.map (c.ι.app j) := rfl
 
+/-- If `H` is an equivalence, we invert `H.map_cone` and get a cone for `F` from a cone
+for `F ⋙ H`.-/
+def map_cone_inv [is_equivalence H]
+  (c : cone (F ⋙ H)) : cone F :=
+(limits.cones.functoriality_equivalence F (as_equivalence H)).inverse.obj c
+
 /-- `map_cone` is the left inverse to `map_cone_inv`. -/
 def map_cone_map_cone_inv {F : J ⥤ D} (H : D ⥤ C) [is_equivalence H] (c : cone (F ⋙ H)) :
   map_cone H (map_cone_inv H c) ≅ c :=
-cones.ext (H.inv_fun_id.app c.X)
-begin
-  intro j,
-  dsimp,
-  rw [comp_id, H.map_comp, is_equivalence.fun_inv_map H, assoc, nat_iso.cancel_nat_iso_hom_left,
-      assoc, is_equivalence.inv_fun_id_inv_comp],
-  dsimp, simp,
-end
+(limits.cones.functoriality_equivalence F (as_equivalence H)).counit_iso.app c
 
 /-- `map_cone` is the right inverse to `map_cone_inv`. -/
 def map_cone_inv_map_cone {F : J ⥤ D} (H : D ⥤ C) [is_equivalence H] (c : cone F) :
   map_cone_inv H (map_cone H c) ≅ c :=
-cones.ext (H.fun_inv_id.app _) (λ j, by simp)
+(limits.cones.functoriality_equivalence F (as_equivalence H)).unit_iso.symm.app c
+/-- If `H` is an equivalence, we invert `H.map_cone` and get a cone for `F` from a cone
+for `F ⋙ H`.-/
+
+def map_cocone_inv [is_equivalence H]
+  (c : cocone (F ⋙ H)) : cocone F :=
+(limits.cocones.functoriality_equivalence F (as_equivalence H)).inverse.obj c
+
+/-- `map_cocone` is the left inverse to `map_cocone_inv`. -/
+def map_cocone_map_cocone_inv {F : J ⥤ D} (H : D ⥤ C) [is_equivalence H] (c : cocone (F ⋙ H)) :
+  map_cocone H (map_cocone_inv H c) ≅ c :=
+(limits.cocones.functoriality_equivalence F (as_equivalence H)).counit_iso.app c
+
+/-- `map_cocone` is the right inverse to `map_cocone_inv`. -/
+def map_cocone_inv_map_cocone {F : J ⥤ D} (H : D ⥤ C) [is_equivalence H] (c : cocone F) :
+  map_cocone_inv H (map_cocone H c) ≅ c :=
+(limits.cocones.functoriality_equivalence F (as_equivalence H)).unit_iso.symm.app c
 
 end functor
 

src/category_theory/limits/limits.lean

@@ -314,7 +314,7 @@ let w' : e.inverse ⋙ F ≅ G := (iso_whisker_left e.inverse w).symm ≪≫ inv
     dsimp,
     simp only [limits.cone.whisker_π, limits.cones.postcompose_obj_π, fac, whisker_left_app,
       assoc, id_comp, inv_fun_id_assoc_hom_app, fac_assoc, nat_trans.comp_app],
-    rw [counit_functor, ←functor.comp_map, w.hom.naturality],
+    rw [counit_app_functor, ←functor.comp_map, w.hom.naturality],
     simp,
   end,
   inv_hom_id' := by { apply hom_ext Q, tidy, }, }
@@ -734,7 +734,7 @@ let w' : e.inverse ⋙ F ≅ G := (iso_whisker_left e.inverse w).symm ≪≫ inv
     dsimp,
     simp only [limits.cocone.whisker_ι, fac, inv_fun_id_assoc_inv_app, whisker_left_app, assoc,
       comp_id, limits.cocones.precompose_obj_ι, fac_assoc, nat_trans.comp_app],
-    rw [←functor_unit, ←functor.comp_map, ←w.inv.naturality_assoc],
+    rw [counit_inv_app_functor, ←functor.comp_map, ←w.inv.naturality_assoc],
     dsimp,
     simp,
   end,

src/category_theory/monoidal/transport.lean

@@ -175,7 +175,7 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
   begin
     dsimp,
     simp only [tensor_id, assoc, id_comp, functor.map_comp, e.inverse.map_id],
-    rw equivalence.counit_functor,
+    rw equivalence.counit_app_functor,
     simp only [←e.functor.map_comp],
     congr' 1,
     rw [←left_unitor_naturality],
@@ -185,7 +185,7 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
   begin
     dsimp,
     simp only [tensor_id, assoc, id_comp, functor.map_comp, e.inverse.map_id],
-    rw equivalence.counit_functor,
+    rw equivalence.counit_app_functor,
     simp only [←e.functor.map_comp],
     congr' 1,
     rw [←right_unitor_naturality],
@@ -271,9 +271,9 @@ monoidal_nat_iso.of_components (λ X, e.counit_iso.app X) (λ X Y f, e.counit.na
   (λ X Y,
   begin
     dsimp, simp only [iso.hom_inv_id_app_assoc, id_comp, equivalence.inv_fun_map],
-    simp only [equivalence.counit_functor, ←e.functor.map_id, ←e.functor.map_comp],
+    simp only [equivalence.counit_app_functor, ←e.functor.map_id, ←e.functor.map_comp],
     congr' 1,
-    simp [equivalence.inverse_counit],
+    simp [equivalence.unit_inv_app_inverse],
     dsimp,
     simp, -- See note [dsimp, simp].
   end)