feat(category_theory/limits): more opposite-related transformations o…

…f cones (#12165)

src/category_theory/limits/cones.lean

@@ -646,30 +646,22 @@ 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, quiver.hom.unop_inj (by tidy) } }
+  π := nat_trans.op c.ι }
 
 /-- 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, quiver.hom.unop_inj (by tidy) } }
+  ι := nat_trans.op c.π }
 
 /-- 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, quiver.hom.op_inj (c.ι.naturality f.op).symm } }
+  π := nat_trans.remove_op c.ι }
 
 /-- 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, quiver.hom.op_inj (c.π.naturality f.op).symm } }
+  ι := nat_trans.remove_op c.π }
 
 variables (F)
 
@@ -694,20 +686,7 @@ def cocone_equivalence_op_cone_op : cocone F ≌ (cone F.op)ᵒᵖ :=
   counit_iso := nat_iso.of_components (λ c,
     by { induction c using opposite.rec,
          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 quiver.hom.unop_inj,
-      apply cone_morphism.ext,
-      dsimp, simp,
-    end,
+    (λ X Y f, quiver.hom.unop_inj (cone_morphism.ext _ _ (by { dsimp, simp }))),
   functor_unit_iso_comp' := λ c, begin apply quiver.hom.unop_inj, ext, dsimp, simp, end }
 
 end
@@ -721,7 +700,7 @@ variables {F : J ⥤ Cᵒᵖ}
 @[simps {rhs_md := semireducible, simp_rhs := tt}]
 def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
 { X := op c.X,
-  π := nat_trans.remove_left_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) }
+  π := nat_trans.remove_left_op c.ι }
 
 /-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.left_op : Jᵒᵖ ⥤ C`. -/
 @[simps {rhs_md := semireducible, simp_rhs := tt}]
@@ -736,11 +715,11 @@ def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
 @[simps X]
 def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
 { X := op c.X,
-  ι := nat_trans.remove_left_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) }
+  ι := nat_trans.remove_left_op 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 :=
-by { dsimp [cocone_of_cone_left_op], simp }
+by { dsimp only [cocone_of_cone_left_op], simp }
 
 /-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.left_op : Jᵒᵖ ⥤ C`. -/
 @[simps {rhs_md := semireducible, simp_rhs := tt}]
@@ -750,6 +729,56 @@ def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
 
 end
 
+section
+variables {F : Jᵒᵖ ⥤ C}
+
+/-- Change a cocone on `F.right_op : J ⥤ Cᵒᵖ` to a cone on `F : Jᵒᵖ ⥤ C`. -/
+@[simps] def cone_of_cocone_right_op (c : cocone F.right_op) : cone F :=
+{ X := unop c.X,
+  π := nat_trans.remove_right_op c.ι }
+
+/-- Change a cone on `F : Jᵒᵖ ⥤ C` to a cocone on `F.right_op : Jᵒᵖ ⥤ C`. -/
+@[simps] def cocone_right_op_of_cone (c : cone F) : cocone (F.right_op) :=
+{ X := op c.X,
+  ι := nat_trans.right_op c.π }
+
+/-- Change a cone on `F.right_op : J ⥤ Cᵒᵖ` to a cocone on `F : Jᵒᵖ ⥤ C`. -/
+@[simps] def cocone_of_cone_right_op (c : cone F.right_op) : cocone F :=
+{ X := unop c.X,
+  ι := nat_trans.remove_right_op c.π }
+
+/-- Change a cocone on `F : Jᵒᵖ ⥤ C` to a cone on `F.right_op : J ⥤ Cᵒᵖ`. -/
+@[simps] def cone_right_op_of_cocone (c : cocone F) : cone (F.right_op) :=
+{ X := op c.X,
+  π := nat_trans.right_op c.ι }
+
+end
+
+section
+variables {F : Jᵒᵖ ⥤ Cᵒᵖ}
+
+/-- Change a cocone on `F.unop : J ⥤ C` into a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
+@[simps] def cone_of_cocone_unop (c : cocone F.unop) : cone F :=
+{ X := op c.X,
+  π := nat_trans.remove_unop c.ι }
+
+/-- Change a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cocone on `F.unop : J ⥤ C`. -/
+@[simps] def cocone_unop_of_cone (c : cone F) : cocone F.unop :=
+{ X := unop c.X,
+  ι := nat_trans.unop c.π }
+
+/-- Change a cone on `F.unop : J ⥤ C` into a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
+@[simps] def cocone_of_cone_unop (c : cone F.unop) : cocone F :=
+{ X := op c.X,
+  ι := nat_trans.remove_unop c.π }
+
+/-- Change a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cone on `F.unop : J ⥤ C`. -/
+@[simps] def cone_unop_of_cocone (c : cocone F) : cone F.unop :=
+{ X := unop c.X,
+  π := nat_trans.unop c.ι }
+
+end
+
 end category_theory.limits
 
 namespace category_theory.functor

src/category_theory/limits/opposites.lean

@@ -43,16 +43,8 @@ has_limit.mk
       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_ι, quiver.hom.unop_op],
-      refl,
+      refine quiver.hom.unop_inj (colimit.hom_ext (λ j, quiver.hom.op_inj _)),
+      simpa only [quiver.hom.unop_op, colimit.ι_desc] using w (unop j)
     end } }
 
 /--
@@ -84,13 +76,8 @@ has_colimit.mk
       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_π, quiver.hom.unop_op],
-      refl,
+      refine quiver.hom.unop_inj (limit.hom_ext (λ j, quiver.hom.op_inj _)),
+      simpa only [quiver.hom.unop_op, limit.lift_π] using w (unop j),
     end } }
 
 /--

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -486,7 +486,7 @@ begin
       apply inter_union_pullback_cone_lift_right },
     all_goals
     { dsimp only [functor.op, pairwise.cocone_ι_app, functor.map_cone_π_app,
-        cocone.op, pairwise.cocone_ι_app_2, unop_op, op_comp],
+        cocone.op, pairwise.cocone_ι_app_2, unop_op, op_comp, nat_trans.op],
       simp_rw [F.1.map_comp, ← category.assoc],
       congr' 1,
       simp_rw [category.assoc, ← F.1.map_comp] },