fix(category_theory/limits): make is_limit a class, clean up proofs (#…

…1187)

* feat(category_theory/limits): equivalences create limits

* equivalence lemma

* add @[simp]

* use right_adjoint_preserves_limits

* blech

* undo weird changes in topology files

* formatting

* do colimits too

* working!

* ?

src/algebra/CommRing/colimits.lean

@@ -428,7 +428,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
 -- FIXME why is this infer_instance needed!?
 instance has_colimits_CommRing : @has_colimits CommRing.{v} infer_instance :=
 { has_colimits_of_shape := λ J 𝒥,
-  { has_colimit := λ F, by resetI; exact
+  { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,
       is_colimit := colimit_is_colimit F } } }
 

src/algebra/Mon/colimits.lean

@@ -229,7 +229,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
 -- FIXME why is this infer_instance needed!?
 instance has_colimits_Mon : @has_colimits Mon.{v} infer_instance :=
 { has_colimits_of_shape := λ J 𝒥,
-  { has_colimit := λ F, by resetI; exact
+  { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,
       is_colimit := colimit_is_colimit F } } }
 

src/category_theory/adjunction/basic.lean

@@ -29,6 +29,14 @@ structure adjunction (F : C ⥤ D) (G : D ⥤ C) :=
 
 infix ` ⊣ `:15 := adjunction
 
+class is_left_adjoint (left : C ⥤ D) :=
+(right : D ⥤ C)
+(adj : left ⊣ right)
+
+class is_right_adjoint (right : D ⥤ C) :=
+(left : C ⥤ D)
+(adj : left ⊣ right)
+
 namespace adjunction
 
 restate_axiom hom_equiv_unit'
@@ -207,14 +215,6 @@ def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
 
 end
 
-structure is_left_adjoint (left : C ⥤ D) :=
-(right : D ⥤ C)
-(adj : left ⊣ right)
-
-structure is_right_adjoint (right : D ⥤ C) :=
-(left : C ⥤ D)
-(adj : left ⊣ right)
-
 section construct_left
 -- Construction of a left adjoint. In order to construct a left
 -- adjoint to a functor G : D → C, it suffices to give the object part

src/category_theory/adjunction/limits.lean

@@ -36,29 +36,24 @@ def functoriality_is_left_adjoint :
 instance left_adjoint_preserves_colimits : preserves_colimits F :=
 { preserves_colimits_of_shape := λ J 𝒥,
   { preserves_colimit := λ F,
-    by resetI; exact
+    by exactI
     { 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 _ ) } } }.
 
 omit adj
 
--- TODO the implicit arguments make preserves_colimit* quite hard to use.
--- This should be refactored at some point. (Possibly including making `is_colimit` a class.)
-def is_colimit_map_cocone (E : C ⥤ D) [is_equivalence E]
+instance is_equivalence_preserves_colimits (E : C ⥤ D) [is_equivalence E] : preserves_colimits E :=
+adjunction.left_adjoint_preserves_colimits E.adjunction
+
+-- verify the preserve_colimits instance works as expected:
+example (E : C ⥤ D) [is_equivalence E]
   (c : cocone K) (h : is_colimit c) : is_colimit (E.map_cocone c) :=
-begin
-  have P : preserves_colimits E := adjunction.left_adjoint_preserves_colimits E.adjunction,
-  have P' := P.preserves_colimits_of_shape,
-  have P'' := P'.preserves_colimit,
-  have P''' := P''.preserves,
-  exact P''' h,
-end
+by apply_instance
 
 instance has_colimit_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimit K] :
   has_colimit (K ⋙ E) :=
-{ cocone := E.map_cocone (colimit.cocone K),
-  is_colimit := is_colimit_map_cocone _ _ _ (colimit.is_colimit K) }
+{ cocone := E.map_cocone (colimit.cocone K) }
 
 def has_colimit_of_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimit (K ⋙ E)] :
   has_colimit K :=
@@ -83,29 +78,24 @@ def functoriality_is_right_adjoint :
 instance right_adjoint_preserves_limits : preserves_limits G :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K,
-    by resetI; exact
+    by exactI
     { 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 _) } } }.
 
 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 is_equivalence_preserves_limits (E : D ⥤ C) [is_equivalence E] : preserves_limits E :=
+adjunction.right_adjoint_preserves_limits E.inv.adjunction
+
+-- 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) :=
+by apply_instance
 
 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) }
+{ cone := E.map_cone (limit.cone K) }
 
 def has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit (K ⋙ E)] :
   has_limit K :=

src/category_theory/limits/limits.lean

@@ -32,6 +32,8 @@ restate_axiom is_limit.fac'
 attribute [simp] is_limit.fac
 restate_axiom is_limit.uniq'
 
+attribute [class] is_limit
+
 namespace is_limit
 
 instance subsingleton {t : cone F} : subsingleton (is_limit t) :=
@@ -142,6 +144,8 @@ restate_axiom is_colimit.fac'
 attribute [simp] is_colimit.fac
 restate_axiom is_colimit.uniq'
 
+attribute [class] is_colimit
+
 namespace is_colimit
 
 instance subsingleton {t : cocone F} : subsingleton (is_colimit t) :=
@@ -246,7 +250,7 @@ section limit
 /-- `has_limit F` represents a particular chosen limit of the diagram `F`. -/
 class has_limit (F : J ⥤ C) :=
 (cone : cone F)
-(is_limit : is_limit cone)
+(is_limit : is_limit cone . tactic.apply_instance)
 
 variables (J C)
 
@@ -284,7 +288,7 @@ def limit.π (F : J ⥤ C) [has_limit F] (j : J) : limit F ⟶ F.obj j :=
 @[simp] lemma limit.w (F : J ⥤ C) [has_limit F] {j j' : J} (f : j ⟶ j') :
   limit.π F j ≫ F.map f = limit.π F j' := (limit.cone F).w f
 
-def limit.is_limit (F : J ⥤ C) [has_limit F] : is_limit (limit.cone F) :=
+instance limit.is_limit (F : J ⥤ C) [has_limit F] : is_limit (limit.cone F) :=
 has_limit.is_limit.{v} F
 
 def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
@@ -327,16 +331,20 @@ lemma limit.lift_extend {F : J ⥤ C} [has_limit F] (c : cone F) {X : C} (f : X
 by obviously
 
 def has_limit_of_iso {F G : J ⥤ C} [has_limit F] (α : F ≅ G) : has_limit G :=
-begin
-  use (cones.postcompose α.hom).obj (limit.cone F),
-  refine ⟨λ s, limit.lift F ((cones.postcompose α.inv).obj s), _, _⟩,
-  { intros s j,
-    rw [cones.postcompose_obj_π, nat_trans.comp_app, limit.cone_π],
-    rw [category.assoc_symm, limit.lift_π], simp },
-  intros s m w, apply limit.hom_ext, intro j,
-  rw [limit.lift_π, cones.postcompose_obj_π, nat_trans.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
-  simpa using w j
-end
+{ cone := (cones.postcompose α.hom).obj (limit.cone F),
+  is_limit :=
+  { lift := λ s, limit.lift F ((cones.postcompose α.inv).obj s),
+    fac' := λ s j,
+    begin
+      rw [cones.postcompose_obj_π, nat_trans.comp_app, limit.cone_π],
+      rw [category.assoc_symm, limit.lift_π], simp
+    end,
+    uniq' := λ s m w,
+    begin
+      apply limit.hom_ext, intro j,
+      rw [limit.lift_π, cones.postcompose_obj_π, nat_trans.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
+      simpa using w j
+    end } }
 
 section pre
 variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
@@ -401,16 +409,21 @@ by ext; erw [assoc, limit.post_π, ←G.map_comp, limit.pre_π, assoc, limit.pre
 
 open category_theory.equivalence
 instance has_limit_equivalence_comp (e : K ≌ J) [has_limit F] : has_limit (e.functor ⋙ F) :=
-begin
-  use cone.whisker e.functor (limit.cone F),
-  let e' := cones.postcompose (e.inv_fun_id_assoc F).hom,
-  refine ⟨λ s, limit.lift F (e'.obj (cone.whisker e.inverse s)), _, _⟩,
-  { intros s j, dsimp, rw [limit.lift_π], dsimp [e'],
-    erw [inv_fun_id_assoc_hom_app, counit_functor, ←s.π.naturality, id_comp] },
-  intros s m w, apply limit.hom_ext, intro j,
-  erw [limit.lift_π, ←limit.w F (e.counit_iso.hom.app j)],
-  slice_lhs 1 2 { erw [w (e.inverse.obj j)] }, simp
-end
+{ cone := cone.whisker e.functor (limit.cone F),
+  is_limit :=
+  let e' := cones.postcompose (e.inv_fun_id_assoc F).hom in
+  { lift := λ s, limit.lift F (e'.obj (cone.whisker e.inverse s)),
+    fac' := λ s j,
+    begin
+      dsimp, rw [limit.lift_π], dsimp [e'],
+      erw [inv_fun_id_assoc_hom_app, counit_functor, ←s.π.naturality, id_comp]
+    end,
+    uniq' := λ s m w,
+    begin
+      apply limit.hom_ext, intro j,
+      erw [limit.lift_π, ←limit.w F (e.counit_iso.hom.app j)],
+      slice_lhs 1 2 { erw [w (e.inverse.obj j)] }, simp
+    end } }
 
 def has_limit_of_equivalence_comp (e : K ≌ J) [has_limit (e.functor ⋙ F)] : has_limit F :=
 begin
@@ -487,7 +500,7 @@ section colimit
 /-- `has_colimit F` represents a particular chosen colimit of the diagram `F`. -/
 class has_colimit (F : J ⥤ C) :=
 (cocone : cocone F)
-(is_colimit : is_colimit cocone)
+(is_colimit : is_colimit cocone . tactic.apply_instance)
 
 variables (J C)
 
@@ -525,7 +538,7 @@ def colimit.ι (F : J ⥤ C) [has_colimit F] (j : J) : F.obj j ⟶ colimit F :=
 @[simp] lemma colimit.w (F : J ⥤ C) [has_colimit F] {j j' : J} (f : j ⟶ j') :
   F.map f ≫ colimit.ι F j' = colimit.ι F j := (colimit.cocone F).w f
 
-def colimit.is_colimit (F : J ⥤ C) [has_colimit F] : is_colimit (colimit.cocone F) :=
+instance colimit.is_colimit (F : J ⥤ C) [has_colimit F] : is_colimit (colimit.cocone F) :=
 has_colimit.is_colimit.{v} F
 
 def colimit.desc (F : J ⥤ C) [has_colimit F] (c : cocone F) : colimit F ⟶ c.X :=
@@ -583,17 +596,21 @@ begin
 end
 
 def has_colimit_of_iso {F G : J ⥤ C} [has_colimit F] (α : G ≅ F) : has_colimit G :=
-begin
-  use (cocones.precompose α.hom).obj (colimit.cocone F),
-  refine ⟨λ s, colimit.desc F ((cocones.precompose α.inv).obj s), _, _⟩,
-  { intros s j,
-    rw [cocones.precompose_obj_ι, nat_trans.comp_app, colimit.cocone_ι],
-    rw [category.assoc, colimit.ι_desc, ←nat_iso.app_hom, ←iso.eq_inv_comp], refl },
-  intros s m w, apply colimit.hom_ext, intro j,
-  rw [colimit.ι_desc, cocones.precompose_obj_ι, nat_trans.comp_app, ←nat_iso.app_inv,
-    iso.eq_inv_comp],
-  simpa using w j
-end
+{ cocone := (cocones.precompose α.hom).obj (colimit.cocone F),
+  is_colimit :=
+  { desc := λ s, colimit.desc F ((cocones.precompose α.inv).obj s),
+    fac' := λ s j,
+    begin
+      rw [cocones.precompose_obj_ι, nat_trans.comp_app, colimit.cocone_ι],
+      rw [category.assoc, colimit.ι_desc, ←nat_iso.app_hom, ←iso.eq_inv_comp], refl
+    end,
+    uniq' := λ s m w,
+    begin
+      apply colimit.hom_ext, intro j,
+      rw [colimit.ι_desc, cocones.precompose_obj_ι, nat_trans.comp_app, ←nat_iso.app_inv,
+        iso.eq_inv_comp],
+      simpa using w j
+    end } }
 
 section pre
 variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
@@ -680,17 +697,21 @@ end
 
 open category_theory.equivalence
 instance has_colimit_equivalence_comp (e : K ≌ J) [has_colimit F] : has_colimit (e.functor ⋙ F) :=
-begin
-  use cocone.whisker e.functor (colimit.cocone F),
-  let e' := cocones.precompose (e.inv_fun_id_assoc F).inv,
-  refine ⟨λ s, colimit.desc F (e'.obj (cocone.whisker e.inverse s)), _, _⟩,
-  { intros s j, dsimp, rw [colimit.ι_desc], dsimp [e'],
-    erw [inv_fun_id_assoc_inv_app, ←functor_unit, s.ι.naturality, comp_id], refl },
-  intros s m w, apply colimit.hom_ext, intro j,
-  erw [colimit.ι_desc],
-  have := w (e.inverse.obj j), simp at this, erw [←colimit.w F (e.counit_iso.hom.app j)] at this,
-  erw [assoc, ←iso.eq_inv_comp (F.map_iso $ e.counit_iso.app j)] at this, erw [this], simp
-end
+{ cocone := cocone.whisker e.functor (colimit.cocone F),
+  is_colimit := let e' := cocones.precompose (e.inv_fun_id_assoc F).inv in
+  { desc := λ s, colimit.desc F (e'.obj (cocone.whisker e.inverse s)),
+    fac' := λ s j,
+    begin
+      dsimp, rw [colimit.ι_desc], dsimp [e'],
+      erw [inv_fun_id_assoc_inv_app, ←functor_unit, s.ι.naturality, comp_id], refl
+    end,
+    uniq' := λ s m w,
+    begin
+      apply colimit.hom_ext, intro j,
+      erw [colimit.ι_desc],
+      have := w (e.inverse.obj j), simp at this, erw [←colimit.w F (e.counit_iso.hom.app j)] at this,
+      erw [assoc, ←iso.eq_inv_comp (F.map_iso $ e.counit_iso.app j)] at this, erw [this], simp
+    end } }
 
 def has_colimit_of_equivalence_comp (e : K ≌ J) [has_colimit (e.functor ⋙ F)] : has_colimit F :=
 begin

src/category_theory/limits/preserves.lean

@@ -46,19 +46,23 @@ with the above definition of "preserves limits".
 -/
 
 class preserves_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
-(preserves : Π {c : cone K}, is_limit c → is_limit (F.map_cone c))
+(preserves : Π {c : cone K} [is_limit c], is_limit (F.map_cone c))
 class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
-(preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c))
+(preserves : Π {c : cocone K} [is_colimit c], is_colimit (F.map_cocone c))
 
 class preserves_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
 (preserves_limit : Π {K : J ⥤ C}, preserves_limit K F)
 class preserves_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
 (preserves_colimit : Π {K : J ⥤ C}, preserves_colimit K F)
 
 class preserves_limits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
-(preserves_limits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI preserves_limits_of_shape J F)
+(preserves_limits_of_shape : Π {J : Type v} [𝒥 : small_category J], by exactI preserves_limits_of_shape J F)
 class preserves_colimits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
-(preserves_colimits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI preserves_colimits_of_shape J F)
+(preserves_colimits_of_shape : Π {J : Type v} [𝒥 : small_category J], by exactI preserves_colimits_of_shape J F)
+
+attribute [instance]
+  preserves_limit.preserves preserves_limits_of_shape.preserves_limit preserves_limits.preserves_limits_of_shape
+  preserves_colimit.preserves preserves_colimits_of_shape.preserves_colimit preserves_colimits.preserves_colimits_of_shape
 
 instance preserves_limit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : subsingleton (preserves_limit K F) :=
 by split; rintros ⟨a⟩ ⟨b⟩; congr
@@ -77,20 +81,6 @@ by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsin
 instance preserves_colimits_subsingleton (F : C ⥤ D) : subsingleton (preserves_colimits F) :=
 by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
 
-instance preserves_limit_of_preserves_limits_of_shape (F : C ⥤ D)
-  [H : preserves_limits_of_shape J F] : preserves_limit K F :=
-preserves_limits_of_shape.preserves_limit J F
-instance preserves_colimit_of_preserves_colimits_of_shape (F : C ⥤ D)
-  [H : preserves_colimits_of_shape J F] : preserves_colimit K F :=
-preserves_colimits_of_shape.preserves_colimit J F
-
-instance preserves_limits_of_shape_of_preserves_limits (F : C ⥤ D)
-  [H : preserves_limits F] : preserves_limits_of_shape J F :=
-preserves_limits.preserves_limits_of_shape F
-instance preserves_colimits_of_shape_of_preserves_colimits (F : C ⥤ D)
-  [H : preserves_colimits F] : preserves_colimits_of_shape J F :=
-preserves_colimits.preserves_colimits_of_shape F
-
 instance id_preserves_limits : preserves_limits (functor.id C) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K, by exactI ⟨λ c h,
@@ -113,11 +103,11 @@ local attribute [elab_simple] preserves_limit.preserves preserves_colimit.preser
 
 instance comp_preserves_limit [preserves_limit K F] [preserves_limit (K ⋙ F) G] :
   preserves_limit K (F ⋙ G) :=
-⟨λ c h, preserves_limit.preserves G (preserves_limit.preserves F h)⟩
+⟨λ c h, by exactI @preserves_limit.preserves _ _ _ _ _ _ (K ⋙ F) G _ _ (preserves_limit.preserves K F)⟩
 
 instance comp_preserves_colimit [preserves_colimit K F] [preserves_colimit (K ⋙ F) G] :
   preserves_colimit K (F ⋙ G) :=
-⟨λ c h, preserves_colimit.preserves G (preserves_colimit.preserves F h)⟩
+⟨λ c h, by exactI @preserves_colimit.preserves _ _ _ _ _ _ (K ⋙ F) G _ _ (preserves_colimit.preserves K F)⟩
 
 end