feat(category_theory/limits): equivalences create limits

src/category_theory/adjunction/basic.lean

@@ -281,6 +281,10 @@ mk_of_hom_equiv
 
 end construct_right
 
+end adjunction
+
+open adjunction
+
 namespace equivalence
 
 def to_adjunction (e : C ≌ D) : e.functor ⊣ e.inverse :=
@@ -289,6 +293,11 @@ mk_of_unit_counit ⟨e.unit, e.counit, by { ext, exact e.functor_unit_comp X },
 
 end equivalence
 
-end adjunction
+namespace functor
+
+def adjunction (E : C ⥤ D) [is_equivalence E] : E ⊣ E.inv :=
+(E.as_equivalence).to_adjunction
+
+end functor
 
 end category_theory

src/category_theory/adjunction/limits.lean

@@ -27,19 +27,19 @@ variables {J : Type v} [small_category J] (K : J ⥤ C)
 def functoriality_is_left_adjoint :
   is_left_adjoint (@cocones.functoriality _ _ _ _ K _ _ F) :=
 { right := (cocones.functoriality G) ⋙ (cocones.precompose
-    (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv)),
+  (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv)),
   adj := mk_of_unit_counit
   { unit := { app := λ c, { hom := adj.unit.app c.X } },
     counit := { app := λ c, { hom := adj.counit.app c.X } } } }
 
 /-- A left adjoint preserves colimits. -/
-def left_adjoint_preserves_colimits : preserves_colimits F :=
+instance left_adjoint_preserves_colimits : preserves_colimits F :=
 { preserves_colimits_of_shape := λ J 𝒥,
   { preserves_colimit := λ F,
     by resetI; exact
     { preserves := λ c hc, is_colimit_iso_unique_cocone_morphism.inv
         (λ s, (((adj.functoriality_is_left_adjoint _).adj).hom_equiv _ _).unique_of_equiv $
-          is_colimit_iso_unique_cocone_morphism.hom hc _ ) } } }
+          is_colimit_iso_unique_cocone_morphism.hom hc _ ) } } }.
 
 end preservation_colimits
 
@@ -49,19 +49,44 @@ variables {J : Type v} [small_category J] (K : J ⥤ D)
 def functoriality_is_right_adjoint :
   is_right_adjoint (@cones.functoriality _ _ _ _ K _ _ G) :=
 { left := (cones.functoriality F) ⋙ (cones.postcompose
-    ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom)),
+  ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom)),
   adj := mk_of_unit_counit
   { unit := { app := λ c, { hom := adj.unit.app c.X, } },
     counit := { app := λ c, { hom := adj.counit.app c.X, } } } }
 
 /-- A right adjoint preserves limits. -/
-def right_adjoint_preserves_limits : preserves_limits G :=
+instance right_adjoint_preserves_limits : preserves_limits G :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K,
     by resetI; exact
     { preserves := λ c hc, is_limit_iso_unique_cone_morphism.inv
         (λ s, (((adj.functoriality_is_right_adjoint _).adj).hom_equiv _ _).symm.unique_of_equiv $
-          is_limit_iso_unique_cone_morphism.hom hc _) } } }
+          is_limit_iso_unique_cone_morphism.hom hc _) } } }.
+
+omit adj
+
+-- TODO the implicit arguments make preserves_limit* quite hard to use.
+-- This should be refactored at some point. (Possibly including making `is_limit` a class.)
+def is_limit_map_cone (E : D ⥤ C) [is_equivalence E]
+  (c : cone K) (h : is_limit c) : is_limit (E.map_cone c) :=
+begin
+  have P : preserves_limits E := adjunction.right_adjoint_preserves_limits E.inv.adjunction,
+  have P' := P.preserves_limits_of_shape,
+  have P'' := P'.preserves_limit,
+  have P''' := P''.preserves,
+  exact P''' h,
+end
+
+instance has_limit_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit K] :
+  has_limit (K ⋙ E) :=
+{ cone := E.map_cone (limit.cone K),
+  is_limit := is_limit_map_cone _ _ _ (limit.is_limit K) }
+
+def has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit (K ⋙ E)] :
+  has_limit K :=
+@has_limit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K
+(@adjunction.has_limit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
+((iso_whisker_left K (fun_inv_id E)) ≪≫ (functor.right_unitor _))
 
 end preservation_limits
 

src/category_theory/equivalence.lean

@@ -48,11 +48,11 @@ lemma counit_def (e : C ≌ D) : e.counit_iso.hom = e.counit := rfl
 lemma unit_inv_def (e : C ≌ D) : e.unit_iso.inv = e.unit_inv := rfl
 lemma counit_inv_def (e : C ≌ D) : e.counit_iso.inv = e.counit_inv := rfl
 
-lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫
+@[simp] lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫
   e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
 e.functor_unit_iso_comp X
 
-lemma counit_inv_functor_comp (e : C ≌ D) (X : C) :
+@[simp] lemma counit_inv_functor_comp (e : C ≌ D) (X : C) :
   e.counit_inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_inv.app X) = 𝟙 (e.functor.obj X) :=
 begin
   erw [iso.inv_eq_inv
@@ -70,7 +70,7 @@ by { erw [←iso.hom_comp_eq_id (e.functor.map_iso (e.unit_iso.app X)), functor_
 
 /-- The other triangle equality. The proof follows the following proof in Globular:
   http://globular.science/1905.001 -/
-lemma unit_inverse_comp (e : C ≌ D) (Y : D) :
+@[simp] lemma unit_inverse_comp (e : C ≌ D) (Y : D) :
   e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   rw [←id_comp _ (e.inverse.map _), ←map_id e.inverse, ←counit_inv_functor_comp, map_comp,
@@ -91,7 +91,7 @@ begin
     (e.counit_iso.app _).hom_inv_id, map_id] }, erw [id_comp, (e.unit_iso.app _).hom_inv_id], refl
 end
 
-lemma inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
+@[simp] lemma inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
   e.inverse.map (e.counit_inv.app Y) ≫ e.unit_inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   erw [iso.inv_eq_inv
@@ -196,7 +196,7 @@ mk' ::
 (inverse    : D ⥤ C)
 (unit_iso   : 𝟭 C ≅ F ⋙ inverse)
 (counit_iso : inverse ⋙ F ≅ 𝟭 D)
-(functor_unit_iso_comp' : ∀(X : C), F.map ((unit_iso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫
+(functor_unit_iso_comp' : ∀ (X : C), F.map ((unit_iso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫
   counit_iso.hom.app (F.obj X) = 𝟙 (F.obj X) . obviously)
 
 restate_axiom is_equivalence.functor_unit_iso_comp'
@@ -264,6 +264,16 @@ begin
   refl
 end
 
+-- We should probably restate many of the lemmas about `equivalence` for `is_equivalence`,
+-- but these are the only ones I need for now.
+@[simp] lemma functor_unit_comp (E : C ⥤ D) [is_equivalence E] (Y) :
+  E.map (((is_equivalence.unit_iso E).hom).app Y) ≫ ((is_equivalence.counit_iso E).hom).app (E.obj Y) = 𝟙 _ :=
+equivalence.functor_unit_comp (E.as_equivalence) Y
+
+@[simp] lemma counit_inv_functor_comp (E : C ⥤ D) [is_equivalence E] (Y) :
+  ((is_equivalence.counit_iso E).inv).app (E.obj Y) ≫ E.map (((is_equivalence.unit_iso E).inv).app Y) = 𝟙 _ :=
+eq_of_inv_eq_inv (functor_unit_comp _ _)
+
 end is_equivalence
 
 class ess_surj (F : C ⥤ D) :=

src/category_theory/limits/cones.lean

@@ -361,6 +361,19 @@ def map_cone   (c : cone F)   : cone (F ⋙ H)   := (cones.functoriality H).obj
 /-- 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
 
+@[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
+
+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 (is_equivalence.unit_iso H).inv) : F ⋙ (H ⋙ inv H) ⟶ _) ≫ (functor.right_unitor _).hom in
+{ 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') :

src/category_theory/limits/limits.lean

@@ -418,6 +418,9 @@ begin
   apply has_limit_of_iso (e.inv_fun_id_assoc F),
 end
 
+-- `has_limit_comp_equivalence` and `has_limit_of_comp_equivalence`
+-- are proved in `category_theory/adjunction/limits.lean`.
+
 section lim_functor
 
 variables [has_limits_of_shape J C]