chore(category_theory/limits): facts about opposites of limit cones (#…

…4250)

Simple facts about limit cones and opposite categories.



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

src/category_theory/adjunction/opposites.lean

@@ -80,11 +80,12 @@ nat_iso.of_components
 /-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/
 def left_adjoint_uniq {F F' : C ⥤ D} {G : D ⥤ C}
   (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' :=
-nat_iso.unop (fully_faithful_cancel_right _ (left_adjoints_coyoneda_equiv adj2 adj1))
+nat_iso.remove_op (fully_faithful_cancel_right _ (left_adjoints_coyoneda_equiv adj2 adj1))
 
 /-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
 def right_adjoint_uniq {F : C ⥤ D} {G G' : D ⥤ C}
   (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' :=
-nat_iso.unop (left_adjoint_uniq (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1))
+nat_iso.remove_op
+  (left_adjoint_uniq (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1))
 
 end adjunction

src/category_theory/limits/cones.lean

@@ -512,8 +512,7 @@ begin
   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],
-  apply comp_id,
-  -- annoyingly `dsimp, simp` leaves it as `c.π.app j ≫ 𝟙 _ = c.π.app j` instead of closing...
+  dsimp, simp,
 end
 
 /-- `map_cone` is the right inverse to `map_cone_inv`. -/
@@ -527,14 +526,88 @@ end category_theory
 
 namespace category_theory.limits
 
+section
+variables {F : J ⥤ C}
+
+/-- Change a `cocone F` into a `cone F.op`. -/
+@[simps] def cocone.op (c : cocone F) : cone F.op :=
+{ X := op c.X,
+  π :=
+  { app := λ j, (c.ι.app (unop j)).op,
+    naturality' := λ j j' f, has_hom.hom.unop_inj (by tidy) } }
+
+/-- Change a `cone F` into a `cocone F.op`. -/
+@[simps] def cone.op (c : cone F) : cocone F.op :=
+{ X := op c.X,
+  ι :=
+  { app := λ j, (c.π.app (unop j)).op,
+    naturality' := λ j j' f, has_hom.hom.unop_inj (by tidy) } }
+
+/-- Change a `cocone F.op` into a `cone F`. -/
+@[simps] def cocone.unop (c : cocone F.op) : cone F :=
+{ X := unop c.X,
+  π :=
+  { app := λ j, (c.ι.app (op j)).unop,
+    naturality' := λ j j' f, has_hom.hom.op_inj
+    begin dsimp, simp only [comp_id], exact (c.w f.op).symm, end } }
+
+/-- Change a `cone F.op` into a `cocone F`. -/
+@[simps] def cone.unop (c : cone F.op) : cocone F :=
+{ X := unop c.X,
+  ι :=
+  { app := λ j, (c.π.app (op j)).unop,
+    naturality' := λ j j' f, has_hom.hom.op_inj
+    begin dsimp, simp only [id_comp], exact (c.w f.op), end } }
+
+variables (F)
+
+/--
+The category of cocones on `F`
+is equivalent to the opposite category of
+the category of cones on the opposite of `F`.
+-/
+@[simps]
+def cocone_equivalence_op_cone_op : cocone F ≌ (cone F.op)ᵒᵖ :=
+{ functor :=
+  { obj := λ c, op (cocone.op c),
+    map := λ X Y f, has_hom.hom.op
+    { hom := f.hom.op,
+      w' := λ j, by { apply has_hom.hom.unop_inj, dsimp, simp, }, } },
+  inverse :=
+  { obj := λ c, cone.unop (unop c),
+    map := λ X Y f,
+    { hom := f.unop.hom.unop,
+      w' := λ j, by { apply has_hom.hom.op_inj, dsimp, simp, }, } },
+  unit_iso := nat_iso.of_components (λ c, cocones.ext (iso.refl _) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ c,
+    by { op_induction c, dsimp, apply iso.op, exact cones.ext (iso.refl _) (by tidy), })
+    begin
+      intros,
+      have hX : X = op (unop X) := rfl,
+      revert hX,
+      generalize : unop X = X',
+      rintro rfl,
+      have hY : Y = op (unop Y) := rfl,
+      revert hY,
+      generalize : unop Y = Y',
+      rintro rfl,
+      apply has_hom.hom.unop_inj,
+      apply cone_morphism.ext,
+      dsimp, simp,
+    end,
+  functor_unit_iso_comp' := λ c, begin apply has_hom.hom.unop_inj, ext, dsimp, simp, end }
+
+end
+
+section
 variables {F : J ⥤ Cᵒᵖ}
 
--- Here and below we only automatically generate the `@[simp]` lemma for the `X` field,
--- as we can be a simpler `rfl` lemma for the components of the natural transformation by hand.
 /-- Change a cocone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
+-- Here and below we only automatically generate the `@[simp]` lemma for the `X` field,
+-- as we can write a simpler `rfl` lemma for the components of the natural transformation by hand.
 @[simps X] 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) }
+  π := nat_trans.remove_left_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) }
 
 @[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 :=
@@ -552,7 +625,7 @@ by { dsimp [cocone_left_op_of_cone], simp }
 /-- Change a cone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
 @[simps X] 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.π) }
+  ι := nat_trans.remove_left_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) }
 
 @[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 :=
@@ -566,4 +639,29 @@ by { dsimp [cocone_of_cone_left_op], simp }
 @[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
+
 end category_theory.limits
+
+namespace category_theory.functor
+
+open category_theory.limits
+
+variables {F : J ⥤ C}
+variables {D : Type u'} [category.{v} D]
+
+section
+variables (G : C ⥤ D)
+
+/-- The opposite cocone of the image of a cone is the image of the opposite cocone. -/
+def map_cone_op (t : cone F) : (G.map_cone t).op ≅ (G.op.map_cocone t.op) :=
+cocones.ext (iso.refl _) (by tidy)
+
+/-- The opposite cone of the image of a cocone is the image of the opposite cone. -/
+def map_cocone_op {t : cocone F} : (G.map_cocone t).op ≅ (G.op.map_cone t.op) :=
+cones.ext (iso.refl _) (by tidy)
+
+end
+
+end category_theory.functor

src/category_theory/limits/limits.lean

@@ -1706,4 +1706,74 @@ by { constructor, intro F, apply has_colimit_of_equivalence_comp e, apply_instan
 
 end colimit
 
+section opposite
+
+/--
+If `t : cone F` is a limit cone, then `t.op : cocone F.op` is a colimit cocone.
+-/
+def is_limit.op {t : cone F} (P : is_limit t) : is_colimit t.op :=
+{ desc := λ s, (P.lift s.unop).op,
+  fac' := λ s j, congr_arg has_hom.hom.op (P.fac s.unop (unop j)),
+  uniq' := λ s m w,
+  begin
+    rw ← P.uniq s.unop m.unop,
+    { refl, },
+    { dsimp, intro j, rw ← w, refl, }
+  end }
+
+/--
+If `t : cocone F` is a colimit cocone, then `t.op : cone F.op` is a limit cone.
+-/
+def is_colimit.op {t : cocone F} (P : is_colimit t) : is_limit t.op :=
+{ lift := λ s, (P.desc s.unop).op,
+  fac' := λ s j, congr_arg has_hom.hom.op (P.fac s.unop (unop j)),
+  uniq' := λ s m w,
+  begin
+    rw ← P.uniq s.unop m.unop,
+    { refl, },
+    { dsimp, intro j, rw ← w, refl, }
+  end }
+
+/--
+If `t : cone F.op` is a limit cone, then `t.unop : cocone F` is a colimit cocone.
+-/
+def is_limit.unop {t : cone F.op} (P : is_limit t) : is_colimit t.unop :=
+{ desc := λ s, (P.lift s.op).unop,
+  fac' := λ s j, congr_arg has_hom.hom.unop (P.fac s.op (op j)),
+  uniq' := λ s m w,
+  begin
+    rw ← P.uniq s.op m.op,
+    { refl, },
+    { dsimp, intro j, rw ← w, refl, }
+  end }
+
+/--
+If `t : cocone F.op` is a colimit cocone, then `t.unop : cone F.` is a limit cone.
+-/
+def is_colimit.unop {t : cocone F.op} (P : is_colimit t) : is_limit t.unop :=
+{ lift := λ s, (P.desc s.op).unop,
+  fac' := λ s j, congr_arg has_hom.hom.unop (P.fac s.op (op j)),
+  uniq' := λ s m w,
+  begin
+    rw ← P.uniq s.op m.op,
+    { refl, },
+    { dsimp, intro j, rw ← w, refl, }
+  end }
+
+/--
+`t : cone F` is a limit cone if and only is `t.op : cocone F.op` is a colimit cocone.
+-/
+def is_limit_equiv_is_colimit_op {t : cone F} : is_limit t ≃ is_colimit t.op :=
+equiv_of_subsingleton_of_subsingleton
+  is_limit.op (λ P, P.unop.of_iso_limit (cones.ext (iso.refl _) (by tidy)))
+
+/--
+`t : cocone F` is a colimit cocone if and only is `t.op : cone F.op` is a limit cone.
+-/
+def is_colimit_equiv_is_limit_op {t : cocone F} : is_colimit t ≃ is_limit t.op :=
+equiv_of_subsingleton_of_subsingleton
+  is_colimit.op (λ P, P.unop.of_iso_colimit (cocones.ext (iso.refl _) (by tidy)))
+
+end opposite
+
 end category_theory.limits

src/category_theory/monad/equiv_mon.lean

@@ -87,28 +87,43 @@ def Mon_to_Monad : Mon_ (C ⥤ C) ⥤ Monad C :=
       finish,
     end,
     ..f.hom } }
+
+namespace Monad_Mon_equiv
 variable {C}
 
 /-- Isomorphism of functors used in `Monad_Mon_equiv` -/
 @[simps]
-def of_to_mon_end_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ :=
+def counit_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ :=
 { hom := { app := λ _, { hom := 𝟙 _ } },
   inv := { app := λ _, { hom := 𝟙 _ } } }
 
+/-- Auxilliary definition for `Monad_Mon_equiv` -/
+@[simps]
+def unit_iso_hom : 𝟭 _ ⟶ Monad_to_Mon C ⋙ Mon_to_Monad C :=
+{ app := λ _, { app := λ _, 𝟙 _ } }
+
+/-- Auxilliary definition for `Monad_Mon_equiv` -/
+@[simps]
+def unit_iso_inv : Monad_to_Mon C ⋙ Mon_to_Monad C ⟶ 𝟭 _ :=
+{ app := λ _, { app := λ _, 𝟙 _ } }
+
 /-- Isomorphism of functors used in `Monad_Mon_equiv` -/
 @[simps]
-def to_of_mon_end_iso : Monad_to_Mon C ⋙ Mon_to_Monad C ≅ 𝟭 _ :=
-{ hom := { app := λ _, { app := λ _, 𝟙 _ } },
-  inv := { app := λ _, { app := λ _, 𝟙 _ } } }
+def unit_iso : 𝟭 _ ≅ Monad_to_Mon C ⋙ Mon_to_Monad C :=
+{ hom := unit_iso_hom,
+  inv := unit_iso_inv }
+
+end Monad_Mon_equiv
+
+open Monad_Mon_equiv
 
-variable (C)
 /-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/
 @[simps]
 def Monad_Mon_equiv : (Monad C) ≌ (Mon_ (C ⥤ C)) :=
 { functor := Monad_to_Mon _,
   inverse := Mon_to_Monad _,
-  unit_iso := to_of_mon_end_iso.symm,
-  counit_iso := of_to_mon_end_iso }
+  unit_iso := unit_iso,
+  counit_iso := counit_iso }
 
 -- Sanity check
 example (A : Monad C) {X : C} : ((Monad_Mon_equiv C).unit_iso.app A).hom.app X = 𝟙 _ := rfl