feat(category_theory/limits/shapes/comm_sq): opposites of is_pullback and is_pushout (#15269)

This PR shows that the dual of a pushout commutative square is a pullback square, and similar other results.
The most basic `comm_sq` API is also moved to a separate file with fewer dependencies so as to prepare for a refactor of lifting properties which shall be based on `comm_sq`.

Author: joelriou

src/category_theory/comm_sq.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.arrow
+
+
+/-!
+# Commutative squares
+
+This file provide an API for commutative squares in categories.
+If `top`, `left`, `right` and `bottom` are four morphisms which are the edges
+of a square, `comm_sq top left right bottom` is the predicate that this
+square is commutative.
+
+The structure `comm_sq` is extended in `category_theory/shapes/limits/comm_sq.lean`
+as `is_pullback` and `is_pushout` in order to define pullback and pushout squares.
+
+## Future work
+
+Refactor `lift_struct` from `arrow.lean` and lifting properties using `comm_sq.lean`.
+
+-/
+
+namespace category_theory
+
+variables {C : Type*} [category C]
+
+/-- The proposition that a square
+```
+  W ---f---> X
+  |          |
+  g          h
+  |          |
+  v          v
+  Y ---i---> Z
+
+```
+is a commuting square.
+-/
+structure comm_sq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop :=
+(w : f ≫ h = g ≫ i)
+
+attribute [reassoc] comm_sq.w
+
+namespace comm_sq
+
+variables {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+
+lemma flip (p : comm_sq f g h i) : comm_sq g f i h := ⟨p.w.symm⟩
+
+lemma of_arrow {f g : arrow C} (h : f ⟶ g) : comm_sq f.hom h.left h.right g.hom := ⟨h.w.symm⟩
+
+/-- The commutative square in the opposite category associated to a commutative square. -/
+lemma op (p : comm_sq f g h i) : comm_sq i.op h.op g.op f.op :=
+⟨by simp only [← op_comp, p.w]⟩
+
+/-- The commutative square associated to a commutative square in the opposite category. -/
+lemma unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+  (p : comm_sq f g h i) : comm_sq i.unop h.unop g.unop f.unop :=
+⟨by simp only [← unop_comp, p.w]⟩
+
+end comm_sq
+
+namespace functor
+
+variables {D : Type*} [category D]
+variables (F : C ⥤ D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+
+lemma map_comm_sq (s : comm_sq f g h i) : comm_sq (F.map f) (F.map g) (F.map h) (F.map i) :=
+⟨by simpa using congr_arg (λ k : W ⟶ Z, F.map k) s.w⟩
+
+end functor
+
+alias functor.map_comm_sq ← comm_sq.map
+
+end category_theory

src/category_theory/limits/shapes/comm_sq.lean

@@ -1,11 +1,13 @@
 /-
 Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Joël Riou
 -/
+import category_theory.comm_sq
 import category_theory.limits.preserves.shapes.pullbacks
 import category_theory.limits.shapes.zero_morphisms
 import category_theory.limits.constructions.binary_products
+import category_theory.limits.opposites
 
 /-!
 # Pullback and pushout squares
@@ -49,31 +51,10 @@ namespace category_theory
 
 variables {C : Type u₁} [category.{v₁} C]
 
-/-- The proposition that a square
-```
-  W ---f---> X
-  |          |
-  g          h
-  |          |
-  v          v
-  Y ---i---> Z
-
-```
-is a commuting square.
--/
-structure comm_sq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop :=
-(w : f ≫ h = g ≫ i)
-
-attribute [reassoc] comm_sq.w
-
 namespace comm_sq
 
 variables {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
 
-lemma flip (p : comm_sq f g h i) : comm_sq g f i h := ⟨p.w.symm⟩
-
-lemma of_arrow {f g : arrow C} (h : f ⟶ g) : comm_sq f.hom h.left h.right g.hom := ⟨h.w.symm⟩
-
 /--
 The (not necessarily limiting) `pullback_cone h i` implicit in the statement
 that we have `comm_sq f g h i`.
@@ -86,6 +67,32 @@ that we have `comm_sq f g h i`.
 -/
 def cocone (s : comm_sq f g h i) : pushout_cocone f g := pushout_cocone.mk _ _ s.w
 
+/-- The pushout cocone in the opposite category associated to the cone of
+a commutative square identifies to the cocone of the flipped commutative square in
+the opposite category -/
+def cone_op (p : comm_sq f g h i) : p.cone.op ≅ p.flip.op.cocone :=
+pushout_cocone.ext (iso.refl _) (by tidy) (by tidy)
+
+/-- The pullback cone in the opposite category associated to the cocone of
+a commutative square identifies to the cone of the flipped commutative square in
+the opposite category -/
+def cocone_op (p : comm_sq f g h i) : p.cocone.op ≅ p.flip.op.cone :=
+pullback_cone.ext (iso.refl _) (by tidy) (by tidy)
+
+/-- The pushout cocone obtained from the pullback cone associated to a
+commutative square in the opposite category identifies to the cocone associated
+to the flipped square. -/
+def cone_unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+  (p : comm_sq f g h i) : p.cone.unop ≅ p.flip.unop.cocone :=
+pushout_cocone.ext (iso.refl _) (by tidy) (by tidy)
+
+/-- The pullback cone obtained from the pushout cone associated to a
+commutative square in the opposite category identifies to the cone associated
+to the flipped square. -/
+def cocone_unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+  (p : comm_sq f g h i) : p.cocone.unop ≅ p.flip.unop.cone :=
+pullback_cone.ext (iso.refl _) (by tidy) (by tidy)
+
 end comm_sq
 
 /-- The proposition that a square
@@ -357,6 +364,17 @@ lemma of_right {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
   is_pullback h₁₁ v₁₁ v₁₂ h₂₁ :=
 (of_bot s.flip p.symm t.flip).flip
 
+lemma op (h : is_pullback fst snd f g) : is_pushout g.op f.op snd.op fst.op :=
+is_pushout.of_is_colimit (is_colimit.of_iso_colimit
+  (limits.pullback_cone.is_limit_equiv_is_colimit_op h.flip.cone h.flip.is_limit)
+  h.to_comm_sq.flip.cone_op)
+
+lemma unop {P X Y Z : Cᵒᵖ} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
+  (h : is_pullback fst snd f g) : is_pushout g.unop f.unop snd.unop fst.unop :=
+is_pushout.of_is_colimit (is_colimit.of_iso_colimit
+  (limits.pullback_cone.is_limit_equiv_is_colimit_unop h.flip.cone h.flip.is_limit)
+  h.to_comm_sq.flip.cone_unop)
+
 end is_pullback
 
 namespace is_pushout
@@ -429,16 +447,24 @@ lemma of_right {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
   is_pushout h₁₂ v₁₂ v₁₃ h₂₂ :=
 (of_bot s.flip p.symm t.flip).flip
 
+lemma op (h : is_pushout f g inl inr) : is_pullback inr.op inl.op g.op f.op :=
+is_pullback.of_is_limit (is_limit.of_iso_limit
+  (limits.pushout_cocone.is_colimit_equiv_is_limit_op h.flip.cocone h.flip.is_colimit)
+  h.to_comm_sq.flip.cocone_op)
+
+lemma unop {Z X Y P : Cᵒᵖ} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P}
+  (h : is_pushout f g inl inr) : is_pullback inr.unop inl.unop g.unop f.unop :=
+is_pullback.of_is_limit (is_limit.of_iso_limit
+  (limits.pushout_cocone.is_colimit_equiv_is_limit_unop h.flip.cocone h.flip.is_colimit)
+  h.to_comm_sq.flip.cocone_unop)
+
 end is_pushout
 
 namespace functor
 
 variables {D : Type u₂} [category.{v₂} D]
 variables (F : C ⥤ D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
 
-lemma map_comm_sq (s : comm_sq f g h i) : comm_sq (F.map f) (F.map g) (F.map h) (F.map i) :=
-⟨by simpa using congr_arg (λ k : W ⟶ Z, F.map k) s.w⟩
-
 lemma map_is_pullback [preserves_limit (cospan h i) F] (s : is_pullback f g h i) :
   is_pullback (F.map f) (F.map g) (F.map h) (F.map i) :=
 -- This is made slightly awkward because `C` and `D` have different universes,
@@ -465,7 +491,6 @@ end
 
 end functor
 
-alias functor.map_comm_sq ← comm_sq.map
 alias functor.map_is_pullback ← is_pullback.map
 alias functor.map_is_pushout ← is_pushout.map