feat(category_theory/limits/opposites): (co)limits in opposite categories (#926)

* (co)limits in opposite categories

* moving lemmas

* moving stuff about complete lattices to separate PR

* renaming category_of_preorder elsewhere

* build limits functor/shape at a time

* removing stray commas, and making one-liners

* remove non-terminal simps

Author: kim-em

src/category_theory/const.lean

@@ -4,6 +4,7 @@
 
 import category_theory.functor_category
 import category_theory.isomorphism
+import category_theory.opposites
 
 universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
@@ -22,11 +23,33 @@ def const : C ⥤ (J ⥤ C) :=
   map := λ X Y f, { app := λ j, f } }
 
 namespace const
+variables {J}
+
 @[simp] lemma obj_obj (X : C) (j : J) : ((const J).obj X).obj j = X := rfl
 @[simp] lemma obj_map (X : C) {j j' : J} (f : j ⟶ j') : ((const J).obj X).map f = 𝟙 X := rfl
 @[simp] lemma map_app {X Y : C} (f : X ⟶ Y) (j : J) : ((const J).map f).app j = f := rfl
+
+def op_obj_op (X : C) :
+  (const Jᵒᵖ).obj (op X) ≅ ((const J).obj X).op :=
+{ hom := { app := λ j, 𝟙 _ },
+  inv := { app := λ j, 𝟙 _ } }
+
+@[simp] lemma op_obj_op_hom_app (X : C) (j : Jᵒᵖ) : (op_obj_op X).hom.app j = 𝟙 _ := rfl
+@[simp] lemma op_obj_op_inv_app (X : C) (j : Jᵒᵖ) : (op_obj_op X).inv.app j = 𝟙 _ := rfl
+
+def op_obj_unop (X : Cᵒᵖ) :
+  (const Jᵒᵖ).obj (unop X) ≅ ((const J).obj X).left_op :=
+{ hom := { app := λ j, 𝟙 _ },
+  inv := { app := λ j, 𝟙 _ } }
+
+-- Lean needs some help with universes here.
+@[simp] lemma op_obj_unop_hom_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).hom.app j = 𝟙 _ := rfl
+@[simp] lemma op_obj_unop_inv_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).inv.app j = 𝟙 _ := rfl
+
 end const
 
+
+
 section
 variables {D : Sort u₃} [𝒟 : category.{v₃} D]
 include 𝒟

src/category_theory/limits/cones.lean

@@ -313,3 +313,53 @@ def map_cocone_morphism {c c' : cocone F} (f : cocone_morphism c c') :
 end functor
 
 end category_theory
+
+namespace category_theory.limits
+
+variables {F : J ⥤ Cᵒᵖ}
+
+def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
+{ X := op c.X,
+  π := nat_trans.right_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) }
+
+@[simp] lemma cone_of_cocone_left_op_X (c : cocone F.left_op) :
+  (cone_of_cocone_left_op c).X = op c.X :=
+rfl
+@[simp] lemma cone_of_cocone_left_op_π_app (c : cocone F.left_op) (j) :
+  (cone_of_cocone_left_op c).π.app j = (c.ι.app (op j)).op :=
+by { dsimp [cone_of_cocone_left_op], simp }
+
+def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
+{ X := unop c.X,
+  ι := nat_trans.left_op c.π }
+
+@[simp] lemma cocone_left_op_of_cone_X (c : cone F) :
+  (cocone_left_op_of_cone c).X = unop c.X :=
+rfl
+@[simp] lemma cocone_left_op_of_cone_ι_app (c : cone F) (j) :
+  (cocone_left_op_of_cone c).ι.app j = (c.π.app (unop j)).unop :=
+by { dsimp [cocone_left_op_of_cone], simp }
+
+def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
+{ X := op c.X,
+  ι := nat_trans.right_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) }
+
+@[simp] lemma cocone_of_cone_left_op_X (c : cone F.left_op) :
+  (cocone_of_cone_left_op c).X = op c.X :=
+rfl
+@[simp] lemma cocone_of_cone_left_op_ι_app (c : cone F.left_op) (j) :
+  (cocone_of_cone_left_op c).ι.app j = (c.π.app (op j)).op :=
+by { dsimp [cocone_of_cone_left_op], simp }
+
+def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
+{ X := unop c.X,
+  π := nat_trans.left_op c.ι }
+
+@[simp] lemma cone_left_op_of_cocone_X (c : cocone F) :
+  (cone_left_op_of_cocone c).X = unop c.X :=
+rfl
+@[simp] lemma cone_left_op_of_cocone_π_app (c : cocone F) (j) :
+  (cone_left_op_of_cocone c).π.app j = (c.ι.app (unop j)).unop :=
+by { dsimp [cone_left_op_of_cocone], simp }
+
+end category_theory.limits

src/category_theory/limits/opposites.lean

@@ -0,0 +1,74 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.limits.limits
+
+universes v u
+
+open category_theory
+open category_theory.functor
+
+namespace category_theory.limits
+
+variables {C : Sort u} [𝒞 : category.{v+1} C]
+include 𝒞
+variables {J : Type v} [small_category J]
+variable (F : J ⥤ Cᵒᵖ)
+
+instance [has_colimit.{v} F.left_op] : has_limit.{v} F :=
+{ cone := cone_of_cocone_left_op (colimit.cocone F.left_op),
+  is_limit :=
+  { lift := λ s, (colimit.desc F.left_op (cocone_left_op_of_cone s)).op,
+    fac' := λ s j,
+    begin
+      rw [cone_of_cocone_left_op_π_app, colimit.cocone_ι, ←op_comp,
+          colimit.ι_desc, cocone_left_op_of_cone_ι_app, has_hom.hom.op_unop],
+      refl, end,
+    uniq' := λ s m w,
+    begin
+      -- It's a pity we can't do this automatically.
+      -- Usually something like this would work by limit.hom_ext,
+      -- but the opposites get in the way of this firing.
+      have u := (colimit.is_colimit F.left_op).uniq (cocone_left_op_of_cone s) (m.unop),
+      convert congr_arg (λ f : _ ⟶ _, f.op) (u _), clear u,
+      intro j,
+      rw [cocone_left_op_of_cone_ι_app, colimit.cocone_ι],
+      convert congr_arg (λ f : _ ⟶ _, f.unop) (w (unop j)), clear w,
+      rw [cone_of_cocone_left_op_π_app, colimit.cocone_ι, has_hom.hom.unop_op],
+      refl,
+    end } }
+
+instance [has_colimits_of_shape.{v} Jᵒᵖ C] : has_limits_of_shape.{v} J Cᵒᵖ :=
+{ has_limit := λ F, by apply_instance }
+
+instance [has_colimits.{v} C] : has_limits.{v} Cᵒᵖ :=
+{ has_limits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
+
+instance [has_limit.{v} F.left_op] : has_colimit.{v} F :=
+{ cocone := cocone_of_cone_left_op (limit.cone F.left_op),
+  is_colimit :=
+  { desc := λ s, (limit.lift F.left_op (cone_left_op_of_cocone s)).op,
+    fac' := λ s j,
+    begin
+      rw [cocone_of_cone_left_op_ι_app, limit.cone_π, ←op_comp,
+          limit.lift_π, cone_left_op_of_cocone_π_app, has_hom.hom.op_unop],
+      refl, end,
+    uniq' := λ s m w,
+    begin
+      have u := (limit.is_limit F.left_op).uniq (cone_left_op_of_cocone s) (m.unop),
+      convert congr_arg (λ f : _ ⟶ _, f.op) (u _), clear u,
+      intro j,
+      rw [cone_left_op_of_cocone_π_app, limit.cone_π],
+      convert congr_arg (λ f : _ ⟶ _, f.unop) (w (unop j)), clear w,
+      rw [cocone_of_cone_left_op_ι_app, limit.cone_π, has_hom.hom.unop_op],
+      refl,
+    end } }
+
+instance [has_limits_of_shape.{v} Jᵒᵖ C] : has_colimits_of_shape.{v} J Cᵒᵖ :=
+{ has_colimit := λ F, by apply_instance }
+
+instance [has_limits.{v} C] : has_colimits.{v} Cᵒᵖ :=
+{ has_colimits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
+
+end category_theory.limits

src/category_theory/opposites.lean

@@ -98,6 +98,7 @@ instance category.opposite : category.{v₁} Cᵒᵖ :=
 @[simp] lemma unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
   (f ≫ g).unop = g.unop ≫ f.unop := rfl
 @[simp] lemma unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) := rfl
+
 @[simp] lemma unop_id_op {X : C} : (𝟙 (op X)).unop = 𝟙 X := rfl
 @[simp] lemma op_id_unop {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X := rfl
 
@@ -154,6 +155,28 @@ definition op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ :=
 
 -- TODO show these form an equivalence
 
+variables {C D}
+
+protected definition left_op (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D :=
+{ obj := λ X, unop (F.obj (unop X)),
+  map := λ X Y f, (F.map f.unop).unop }
+
+@[simp] lemma left_op_obj (F : C ⥤ Dᵒᵖ) (X : Cᵒᵖ) : (F.left_op).obj X = unop (F.obj (unop X)) := rfl
+@[simp] lemma left_op_map (F : C ⥤ Dᵒᵖ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+  (F.left_op).map f = (F.map f.unop).unop :=
+rfl
+
+protected definition right_op (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ :=
+{ obj := λ X, op (F.obj (op X)),
+  map := λ X Y f, (F.map f.op).op }
+
+@[simp] lemma right_op_obj (F : Cᵒᵖ ⥤ D) (X : C) : (F.right_op).obj X = op (F.obj (op X)) := rfl
+@[simp] lemma right_op_map (F : Cᵒᵖ ⥤ D) {X Y : C} (f : X ⟶ Y) :
+  (F.right_op).map f = (F.map f.op).op :=
+rfl
+
+-- TODO show these form an equivalence
+
 instance {F : C ⥤ D} [full F] : full F.op :=
 { preimage := λ X Y f, (F.preimage f.unop).op }
 
@@ -182,6 +205,50 @@ end
 
 end functor
 
+namespace nat_trans
+
+variables {D : Sort u₂} [𝒟 : category.{v₂} D]
+include 𝒟
+
+section
+variables {F G : C ⥤ D}
+
+protected definition op (α : F ⟶ G) : G.op ⟶ F.op :=
+{ app         := λ X, (α.app (unop X)).op,
+  naturality' := begin tidy, erw α.naturality, refl, end }
+
+@[simp] lemma op_app (α : F ⟶ G) (X) : (nat_trans.op α).app X = (α.app (unop X)).op := rfl
+
+protected definition unop (α : F.op ⟶ G.op) : G ⟶ F :=
+{ app         := λ X, (α.app (op X)).unop,
+  naturality' := begin tidy, erw α.naturality, refl, end }
+
+@[simp] lemma unop_app (α : F.op ⟶ G.op) (X) : (nat_trans.unop α).app X = (α.app (op X)).unop := rfl
+
+end
+
+section
+variables {F G : C ⥤ Dᵒᵖ}
+
+protected definition left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op :=
+{ app         := λ X, (α.app (unop X)).unop,
+  naturality' := begin tidy, erw α.naturality, refl, end }
+
+@[simp] lemma left_op_app (α : F ⟶ G) (X) :
+  (nat_trans.left_op α).app X = (α.app (unop X)).unop :=
+rfl
+
+protected definition right_op (α : F.left_op ⟶ G.left_op) : G ⟶ F :=
+{ app         := λ X, (α.app (op X)).op,
+  naturality' := begin tidy, erw α.naturality, refl, end }
+
+@[simp] lemma right_op_app (α : F.left_op ⟶ G.left_op) (X) :
+  (nat_trans.right_op α).app X = (α.app (op X)).op :=
+rfl
+
+end
+end nat_trans
+
 -- TODO the following definitions do not belong here
 
 omit 𝒞

src/category_theory/yoneda.lean

@@ -161,7 +161,8 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
     erw [←functor_to_types.naturality,
          obj_map_id,
          functor_to_types.naturality,
-         functor_to_types.map_id], refl,
+         functor_to_types.map_id],
+    refl,
   end,
   inv_hom_id' :=
   begin