feat(category_theory/limits): realise products as pullbacks (#14322)

This was mostly done in #10581, this just adds the isomorphisms between the objects produced by the `has_limit` API.



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

src/category_theory/limits/constructions/binary_products.lean

@@ -63,32 +63,43 @@ begin
   { exact h₂.trans (H₂.fac (binary_fan.mk s.fst s.snd) ⟨walking_pair.right⟩).symm }
 end
 
+/-- Any category with pullbacks and a terminal object has a limit cone for each walking pair. -/
+noncomputable def limit_cone_of_terminal_and_pullbacks [has_terminal C] [has_pullbacks C]
+  (F : discrete walking_pair ⥤ C) : limit_cone F :=
+{ cone :=
+  { X := pullback (terminal.from (F.obj ⟨walking_pair.left⟩))
+                  (terminal.from (F.obj ⟨walking_pair.right⟩)),
+    π := discrete.nat_trans (λ x, discrete.cases_on x
+      (λ x, walking_pair.cases_on x pullback.fst pullback.snd)) },
+  is_limit :=
+  { lift := λ c, pullback.lift ((c.π).app ⟨walking_pair.left⟩)
+                                ((c.π).app ⟨walking_pair.right⟩)
+                                (subsingleton.elim _ _),
+    fac' := λ s c, discrete.cases_on c
+      (λ c, walking_pair.cases_on c (limit.lift_π _ _) (limit.lift_π _ _)),
+    uniq' := λ s m J,
+              begin
+                rw [←J, ←J],
+                ext;
+                rw limit.lift_π;
+                refl
+              end } }
+
 variable (C)
 
 /-- Any category with pullbacks and terminal object has binary products. -/
 -- This is not an instance, as it is not always how one wants to construct binary products!
 lemma has_binary_products_of_terminal_and_pullbacks
   [has_terminal C] [has_pullbacks C] :
   has_binary_products C :=
-{ has_limit := λ F, has_limit.mk
-  { cone :=
-    { X := pullback (terminal.from (F.obj ⟨walking_pair.left⟩))
-                    (terminal.from (F.obj ⟨walking_pair.right⟩)),
-      π := discrete.nat_trans (λ x, discrete.cases_on x
-        (λ x, walking_pair.cases_on x pullback.fst pullback.snd)) },
-    is_limit :=
-    { lift := λ c, pullback.lift ((c.π).app ⟨walking_pair.left⟩)
-                                  ((c.π).app ⟨walking_pair.right⟩)
-                                  (subsingleton.elim _ _),
-      fac' := λ s c, discrete.cases_on c
-        (λ c, walking_pair.cases_on c (limit.lift_π _ _) (limit.lift_π _ _)),
-      uniq' := λ s m J,
-                begin
-                  rw [←J, ←J],
-                  ext;
-                  rw limit.lift_π;
-                  refl
-                end } } }
+{ has_limit := λ F, has_limit.mk (limit_cone_of_terminal_and_pullbacks F) }
+
+/-- In a category with a terminal object and pullbacks,
+a product of objects `X` and `Y` is isomorphic to a pullback. -/
+noncomputable
+def prod_iso_pullback [has_terminal C] [has_pullbacks C] (X Y : C) [has_binary_product X Y] :
+  X ⨯ Y ≅ pullback (terminal.from X) (terminal.from Y) :=
+limit.iso_limit_cone (limit_cone_of_terminal_and_pullbacks _)
 
 variable {C}
 
@@ -133,29 +144,40 @@ begin
   { exact h₂.trans (H₂.fac (binary_cofan.mk s.inl s.inr) ⟨walking_pair.right⟩).symm }
 end
 
+/-- Any category with pushouts and an initial object has a colimit cocone for each walking pair. -/
+noncomputable def colimit_cocone_of_initial_and_pushouts [has_initial C] [has_pushouts C]
+  (F : discrete walking_pair ⥤ C) : colimit_cocone F :=
+{ cocone :=
+  { X := pushout (initial.to (F.obj ⟨walking_pair.left⟩))
+                  (initial.to (F.obj ⟨walking_pair.right⟩)),
+    ι := discrete.nat_trans (λ x, discrete.cases_on x
+      (λ x, walking_pair.cases_on x pushout.inl pushout.inr)) },
+  is_colimit :=
+  { desc := λ c, pushout.desc (c.ι.app ⟨walking_pair.left⟩)
+                              (c.ι.app ⟨walking_pair.right⟩)
+                              (subsingleton.elim _ _),
+    fac' := λ s c, discrete.cases_on c
+      (λ c, walking_pair.cases_on c (colimit.ι_desc _ _) (colimit.ι_desc _ _)),
+    uniq' := λ s m J,
+              begin
+                rw [←J, ←J],
+                ext;
+                rw colimit.ι_desc;
+                refl
+              end } }
+
 variable (C)
 
 /-- Any category with pushouts and initial object has binary coproducts. -/
 -- This is not an instance, as it is not always how one wants to construct binary coproducts!
 lemma has_binary_coproducts_of_initial_and_pushouts
   [has_initial C] [has_pushouts C] :
   has_binary_coproducts C :=
-{ has_colimit := λ F, has_colimit.mk
-  { cocone :=
-    { X := pushout (initial.to (F.obj ⟨walking_pair.left⟩))
-                    (initial.to (F.obj ⟨walking_pair.right⟩)),
-      ι := discrete.nat_trans (λ x, discrete.cases_on x
-        (λ x, walking_pair.cases_on x pushout.inl pushout.inr)) },
-    is_colimit :=
-    { desc := λ c, pushout.desc (c.ι.app ⟨walking_pair.left⟩)
-                                (c.ι.app ⟨walking_pair.right⟩)
-                                (subsingleton.elim _ _),
-      fac' := λ s c, discrete.cases_on c
-        (λ c, walking_pair.cases_on c (colimit.ι_desc _ _) (colimit.ι_desc _ _)),
-      uniq' := λ s m J,
-                begin
-                  rw [←J, ←J],
-                  ext;
-                  rw colimit.ι_desc;
-                  refl
-                end } } }
+{ has_colimit := λ F, has_colimit.mk (colimit_cocone_of_initial_and_pushouts F) }
+
+/-- In a category with an initial object and pushouts,
+a coproduct of objects `X` and `Y` is isomorphic to a pushout. -/
+noncomputable
+def coprod_iso_pushout [has_initial C] [has_pushouts C] (X Y : C) [has_binary_coproduct X Y] :
+  X ⨿ Y ≅ pushout (initial.to X) (initial.to Y) :=
+colimit.iso_colimit_cocone (colimit_cocone_of_initial_and_pushouts _)