feat(category_theory): creation of limits and reflection of isomorphi…

…sms (#2426)

Define creation of limits and reflection of isomorphisms.

Part 2 of a sequence of PRs aiming to resolve my TODO [here](https://github.com/leanprover-community/mathlib/blob/cf89963e14cf535783cefba471247ae4470fa8c3/src/category_theory/limits/over.lean#L143) - that the forgetful functor from the over category creates connected limits.

Remaining:

- [x] Add an instance or def which gives that if `F` creates limits and `K ⋙ F` `has_limit` then `has_limit K` as well.
- [x] Move the forget creates limits proof to limits/over, and remove the existing proof since this one is strictly stronger - make sure to keep the statement there though using the previous point.
- [x] Add more docstrings

Probably relevant to @semorrison and @TwoFX.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

src/category_theory/adjunction/limits.lean

@@ -25,19 +25,19 @@ section preservation_colimits
 variables {J : Type v} [small_category J] (K : J ⥤ C)
 
 def functoriality_right_adjoint : cocone (K ⋙ F) ⥤ cocone K :=
-(cocones.functoriality G) ⋙
+(cocones.functoriality _ G) ⋙
   (cocones.precompose (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv))
 
 local attribute [reducible] functoriality_right_adjoint
 
-@[simps] def functoriality_unit : 𝟭 (cocone K) ⟶ cocones.functoriality F ⋙ functoriality_right_adjoint adj K :=
+@[simps] def functoriality_unit : 𝟭 (cocone K) ⟶ cocones.functoriality _ F ⋙ functoriality_right_adjoint adj K :=
 { app := λ c, { hom := adj.unit.app c.X } }
 
-@[simps] def functoriality_counit : functoriality_right_adjoint adj K ⋙ cocones.functoriality F ⟶ 𝟭 (cocone (K ⋙ F)) :=
+@[simps] def functoriality_counit : functoriality_right_adjoint adj K ⋙ cocones.functoriality _ F ⟶ 𝟭 (cocone (K ⋙ F)) :=
 { app := λ c, { hom := adj.counit.app c.X } }
 
 def functoriality_is_left_adjoint :
-  is_left_adjoint (@cocones.functoriality _ _ _ _ K _ _ F) :=
+  is_left_adjoint (cocones.functoriality K F) :=
 { right := functoriality_right_adjoint adj K,
   adj := mk_of_unit_counit
   { unit := functoriality_unit adj K,
@@ -80,19 +80,19 @@ section preservation_limits
 variables {J : Type v} [small_category J] (K : J ⥤ D)
 
 def functoriality_left_adjoint : cone (K ⋙ G) ⥤ cone K :=
-(cones.functoriality F) ⋙ (cones.postcompose
+(cones.functoriality _ F) ⋙ (cones.postcompose
     ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom))
 
 local attribute [reducible] functoriality_left_adjoint
 
-@[simps] def functoriality_unit' : 𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality G :=
+@[simps] def functoriality_unit' : 𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality _ G :=
 { app := λ c, { hom := adj.unit.app c.X, } }
 
-@[simps] def functoriality_counit' : cones.functoriality G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
+@[simps] def functoriality_counit' : cones.functoriality _ G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
 { app := λ c, { hom := adj.counit.app c.X, } }
 
 def functoriality_is_right_adjoint :
-  is_right_adjoint (@cones.functoriality _ _ _ _ K _ _ G) :=
+  is_right_adjoint (cones.functoriality K G) :=
 { left := functoriality_left_adjoint adj K,
   adj := mk_of_unit_counit
   { unit := functoriality_unit' adj K,
@@ -113,6 +113,20 @@ omit adj
 instance is_equivalence_preserves_limits (E : D ⥤ C) [is_equivalence E] : preserves_limits E :=
 right_adjoint_preserves_limits E.inv.adjunction
 
+@[priority 100] -- see Note [lower instance priority]
+instance is_equivalence_reflects_limits (E : D ⥤ C) [is_equivalence E] : reflects_limits E :=
+{ reflects_limits_of_shape := λ J 𝒥, by exactI
+  { reflects_limit := λ K,
+    { reflects := λ c t,
+      begin
+        have l: is_limit (E.inv.map_cone (E.map_cone c)) := preserves_limit.preserves t,
+        convert is_limit.map_cone_equiv E.fun_inv_id l,
+        { rw functor.comp_id },
+        { cases c,
+          cases c_π,
+          congr; rw functor.comp_id }
+      end } } }
+
 -- verify the preserve_limits instance works as expected:
 example (E : D ⥤ C) [is_equivalence E]
   (c : cone K) [h : is_limit c] : is_limit (E.map_cone c) :=

src/category_theory/limits/cones.lean

@@ -213,9 +213,7 @@ variable (F)
 @[simps]
 def forget : cone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
-end
 
-section
 variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
 
@@ -276,9 +274,7 @@ variable (F)
 @[simps]
 def forget : cocone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
-end
 
-section
 variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
 
@@ -302,13 +298,14 @@ variables {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D)
 open category_theory.limits
 
 /-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/
-def map_cone   (c : cone F)   : cone (F ⋙ H)   := (cones.functoriality H).obj c
+def map_cone   (c : cone F)   : cone (F ⋙ H)   := (cones.functoriality F H).obj c
 /-- The image of a cocone in C under a functor G : C ⥤ D is a cocone in D. -/
-def map_cocone (c : cocone F) : cocone (F ⋙ H) := (cocones.functoriality H).obj c
+def map_cocone (c : cocone F) : cocone (F ⋙ H) := (cocones.functoriality F H).obj c
 
 @[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
 
+@[simps]
 def map_cone_inv [is_equivalence H]
   (c : cone (F ⋙ H)) : cone F :=
 let t := (inv H).map_cone c in
@@ -317,18 +314,31 @@ let α : (F ⋙ H) ⋙ inv H ⟶ F :=
 { X := t.X,
   π := ((category_theory.cones J C).map α).app (op t.X) t.π }
 
-@[simp] lemma map_cone_inv_X [is_equivalence H] (c : cone (F ⋙ H)) : (H.map_cone_inv c).X = (inv H).obj c.X := rfl
-
-def map_cone_morphism   {c c' : cone F}   (f : cone_morphism c c')   :
-  cone_morphism   (H.map_cone c)   (H.map_cone c')   := (cones.functoriality H).map f
-def map_cocone_morphism {c c' : cocone F} (f : cocone_morphism c c') :
-  cocone_morphism (H.map_cocone c) (H.map_cocone c') := (cocones.functoriality H).map f
+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
+def map_cocone_morphism {c c' : cocone F} (f : c ⟶ c') :
+  (H.map_cocone c) ⟶ (H.map_cocone c') := (cocones.functoriality F H).map f
 
 @[simp] lemma map_cone_π (c : cone F) (j : J) :
   (map_cone H c).π.app j = H.map (c.π.app j) := rfl
 @[simp] lemma map_cocone_ι (c : cocone F) (j : J) :
   (map_cocone H c).ι.app j = H.map (c.ι.app j) := rfl
 
+/-- `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 :=
+begin
+  apply cones.ext _ (λ j, _),
+  { exact H.inv_fun_id.app c.X },
+  { dsimp,
+    erw [comp_id, ← H.inv_fun_id.hom.naturality (c.π.app j), comp_map, H.map_comp],
+    congr' 1,
+    erw [← cancel_epi (H.inv_fun_id.inv.app (H.obj (F.obj j))), nat_iso.inv_hom_id_app,
+         ← (functor.as_equivalence H).functor_unit _, ← H.map_comp, nat_iso.hom_inv_id_app,
+         H.map_id],
+    refl }
+end
+
 end functor
 
 end category_theory