feat(category_theory/limits): pushouts and pullbacks in the opposite …

…category (#13495)

This PR adds duality isomorphisms for the categories `wide_pushout_shape`, `wide_pullback_shape`, `walking_span`, `walking_cospan` and produce pullbacks/pushouts in the opposite category when pushouts/pullbacks exist.

src/category_theory/limits/opposites.lean

@@ -10,7 +10,7 @@ import category_theory.discrete_category
 # Limits in `C` give colimits in `Cᵒᵖ`.
 
 We also give special cases for (co)products,
-but not yet for pullbacks / pushouts or for (co)equalizers.
+(co)equalizers, and pullbacks / pushouts.
 
 -/
 
@@ -315,4 +315,18 @@ lemma has_finite_limits_opposite [has_finite_colimits C] :
   has_finite_limits Cᵒᵖ :=
 { out := λ J 𝒟 𝒥, by { resetI, apply_instance, }, }
 
+lemma has_pullbacks_opposite [has_pushouts C] : has_pullbacks Cᵒᵖ :=
+begin
+  haveI : has_colimits_of_shape walking_cospan.{v₁}ᵒᵖ C :=
+    has_colimits_of_shape_of_equivalence walking_cospan_op_equiv.symm,
+  apply has_limits_of_shape_op_of_has_colimits_of_shape,
+end
+
+lemma has_pushouts_opposite [has_pullbacks C] : has_pushouts Cᵒᵖ :=
+begin
+  haveI : has_limits_of_shape walking_span.{v₁}ᵒᵖ C :=
+    has_limits_of_shape_of_equivalence walking_span_op_equiv.symm,
+  apply has_colimits_of_shape_op_of_has_limits_of_shape,
+end
+
 end category_theory.limits

src/category_theory/limits/shapes/pullbacks.lean

@@ -2157,4 +2157,12 @@ lemma has_pushouts_of_has_colimit_span
   has_pushouts C :=
 { has_colimit := λ F, has_colimit_of_iso (diagram_iso_span F) }
 
+/-- The duality equivalence `walking_spanᵒᵖ ≌ walking_cospan` -/
+def walking_span_op_equiv : walking_spanᵒᵖ ≌ walking_cospan :=
+wide_pushout_shape_op_equiv _
+
+/-- The duality equivalence `walking_cospanᵒᵖ ≌ walking_span` -/
+def walking_cospan_op_equiv : walking_cospanᵒᵖ ≌ walking_span :=
+wide_pullback_shape_op_equiv _
+
 end category_theory.limits

src/category_theory/limits/shapes/wide_pullbacks.lean

@@ -26,7 +26,7 @@ pullbacks and finite wide pullbacks.
 
 universes v u
 
-open category_theory category_theory.limits
+open category_theory category_theory.limits opposite
 
 namespace category_theory.limits
 
@@ -371,4 +371,78 @@ end
 
 end wide_pushout
 
+variable (J)
+
+/-- The action on morphisms of the obvious functor
+  `wide_pullback_shape_op : wide_pullback_shape J ⥤ (wide_pushout_shape J)ᵒᵖ`-/
+def wide_pullback_shape_op_map : Π (X Y : wide_pullback_shape J),
+  (X ⟶ Y) → ((op X : (wide_pushout_shape J)ᵒᵖ) ⟶ (op Y : (wide_pushout_shape J)ᵒᵖ))
+| _ _ (wide_pullback_shape.hom.id X) := quiver.hom.op (wide_pushout_shape.hom.id _)
+| _ _ (wide_pullback_shape.hom.term j) := quiver.hom.op (wide_pushout_shape.hom.init _)
+
+/-- The obvious functor `wide_pullback_shape J ⥤ (wide_pushout_shape J)ᵒᵖ` -/
+@[simps]
+def wide_pullback_shape_op : wide_pullback_shape J ⥤ (wide_pushout_shape J)ᵒᵖ :=
+{ obj := λ X, op X,
+  map := wide_pullback_shape_op_map J, }
+
+/-- The action on morphisms of the obvious functor
+`wide_pushout_shape_op : `wide_pushout_shape J ⥤ (wide_pullback_shape J)ᵒᵖ` -/
+def wide_pushout_shape_op_map : Π (X Y : wide_pushout_shape J),
+  (X ⟶ Y) → ((op X : (wide_pullback_shape J)ᵒᵖ) ⟶ (op Y : (wide_pullback_shape J)ᵒᵖ))
+| _ _ (wide_pushout_shape.hom.id X) := quiver.hom.op (wide_pullback_shape.hom.id _)
+| _ _ (wide_pushout_shape.hom.init j) := quiver.hom.op (wide_pullback_shape.hom.term _)
+
+/-- The obvious functor `wide_pushout_shape J ⥤ (wide_pullback_shape J)ᵒᵖ` -/
+@[simps]
+def wide_pushout_shape_op : wide_pushout_shape J ⥤ (wide_pullback_shape J)ᵒᵖ :=
+{ obj := λ X, op X,
+  map := wide_pushout_shape_op_map J, }
+
+/-- The obvious functor `(wide_pullback_shape J)ᵒᵖ ⥤ wide_pushout_shape J`-/
+@[simps]
+def wide_pullback_shape_unop : (wide_pullback_shape J)ᵒᵖ ⥤ wide_pushout_shape J :=
+(wide_pullback_shape_op J).left_op
+
+/-- The obvious functor `(wide_pushout_shape J)ᵒᵖ ⥤ wide_pullback_shape J` -/
+@[simps]
+def wide_pushout_shape_unop : (wide_pushout_shape J)ᵒᵖ ⥤ wide_pullback_shape J :=
+(wide_pushout_shape_op J).left_op
+
+/-- The inverse of the unit isomorphism of the equivalence
+`wide_pushout_shape_op_equiv : (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J` -/
+def wide_pushout_shape_op_unop : wide_pushout_shape_unop J ⋙ wide_pullback_shape_op J ≅ 𝟭 _ :=
+nat_iso.of_components (λ X, iso.refl _) (λ X Y f, dec_trivial)
+
+/-- The counit isomorphism of the equivalence
+`wide_pullback_shape_op_equiv : (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J` -/
+def wide_pushout_shape_unop_op : wide_pushout_shape_op J ⋙ wide_pullback_shape_unop J ≅ 𝟭 _ :=
+nat_iso.of_components (λ X, iso.refl _) (λ X Y f, dec_trivial)
+
+/-- The inverse of the unit isomorphism of the equivalence
+`wide_pullback_shape_op_equiv : (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J` -/
+def wide_pullback_shape_op_unop : wide_pullback_shape_unop J ⋙ wide_pushout_shape_op J ≅ 𝟭 _ :=
+nat_iso.of_components (λ X, iso.refl _) (λ X Y f, dec_trivial)
+
+/-- The counit isomorphism of the equivalence
+`wide_pushout_shape_op_equiv : (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J` -/
+def wide_pullback_shape_unop_op : wide_pullback_shape_op J ⋙ wide_pushout_shape_unop J ≅ 𝟭 _ :=
+nat_iso.of_components (λ X, iso.refl _) (λ X Y f, dec_trivial)
+
+/-- The duality equivalence `(wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J` -/
+@[simps]
+def wide_pushout_shape_op_equiv : (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J :=
+{ functor := wide_pushout_shape_unop J,
+  inverse := wide_pullback_shape_op J,
+  unit_iso := (wide_pushout_shape_op_unop J).symm,
+  counit_iso := wide_pullback_shape_unop_op J, }
+
+/-- The duality equivalence `(wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J` -/
+@[simps]
+def wide_pullback_shape_op_equiv : (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J :=
+{ functor := wide_pullback_shape_unop J,
+  inverse := wide_pushout_shape_op J,
+  unit_iso := (wide_pullback_shape_op_unop J).symm,
+  counit_iso := wide_pushout_shape_unop_op J, }
+
 end category_theory.limits