feat(category_theory/limits): pullbacks from binary products and equ…

…alizers (#2143)

* feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y)

* Rename *_of_diagram to diagram_iso_*

* feat(category_theory/limits): pullbacks from binary products and equalizers

* Fix build

* Fix indentation

* typos

* Fix proof

* Remove some simp lemmas that were duplicated during merge

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/category_theory/limits/over.lean

@@ -166,11 +166,8 @@ begin
     (pullback.fst ≫ Y.hom : pullback f.left g.left ⟶ B) = (s.X).hom, simp, refl,
   intros s j, simp, ext1, dsimp,
   cases j, simp, simp, simp,
-  show _ ≫ (((pullback_cone.mk π₁ π₂ _).π).app walking_cospan.one).left = ((s.π).app walking_cospan.one).left,
   dunfold pullback_cone.mk, dsimp,
-  show pullback.lift (((s.π).app walking_cospan.left).left) (((s.π).app walking_cospan.right).left) _ ≫
-    pullback.fst ≫ f.left =
-  ((s.π).app walking_cospan.one).left, simp, rw ← over.comp_left, rw ← s.w walking_cospan.hom.inl,
+  simp, rw ← over.comp_left, rw ← s.w walking_cospan.hom.inl,
   intros s m J, apply over.over_morphism.ext, simp, apply pullback.hom_ext,
   simp at J, dsimp at J,
   have := J walking_cospan.left, dsimp at this, simp, rw ← this, simp,

src/category_theory/limits/shapes/constructions/equalizers.lean

@@ -60,7 +60,7 @@ def equalizer_cone_is_limit (F : walking_parallel_pair ⥤ C) : is_limit (equali
     apply limit.hom_ext,
     rintro (_ | _); simp
   end,
-  fac' := by rintro c (_ | _); simp,
+  fac' := by rintros c (_ | _); simp,
   uniq' :=
   begin
     intros c _ J,

src/category_theory/limits/shapes/constructions/pullbacks.lean

@@ -1 +1,86 @@
--- TODO construct pullbacks from binary products and equalizers
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+
+import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.equalizers
+import category_theory.limits.shapes.pullbacks
+
+universes v u
+
+/-!
+# Constructing pullbacks from binary products and equalizers
+
+If a category as binary products and equalizers, then it has pullbacks.
+Also, if a category has binary coproducts and coequalizers, then it has pushouts
+-/
+
+open category_theory
+
+namespace category_theory.limits
+
+/-- If the product `X ⨯ Y` and the equalizer of `π₁ ≫ f` and `π₂ ≫ g` exist, then the
+    pullback of `f` and `g` exists: It is given by composing the equalizer with the projections. -/
+def has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair
+  {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [has_limit (pair X Y)]
+  [has_limit (parallel_pair (prod.fst ≫ f) (prod.snd ≫ g))] : has_limit (cospan f g) :=
+let π₁ : X ⨯ Y ⟶ X := prod.fst, π₂ : X ⨯ Y ⟶ Y := prod.snd, e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g) in
+{ cone := pullback_cone.mk (e ≫ π₁) (e ≫ π₂) $ by simp only [category.assoc, equalizer.condition],
+  is_limit := pullback_cone.is_limit.mk _
+    (λ s, equalizer.lift (π₁ ≫ f) (π₂ ≫ g) (prod.lift (s.π.app walking_cospan.left)
+      (s.π.app walking_cospan.right)) $ by
+        rw [←category.assoc, limit.lift_π, ←category.assoc, limit.lift_π];
+        exact pullback_cone.condition _)
+    (by simp) (by simp) $ λ s m h, by
+      ext; simp only [limit.lift_π, fork.of_ι_app_zero, category.assoc];
+      exact walking_pair.cases_on j (h walking_cospan.left) (h walking_cospan.right) }
+
+section
+
+local attribute [instance] has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair
+
+/-- If a category has all binary products and all equalizers, then it also has all pullbacks.
+    As usual, this is not an instance, since there may be a more direct way to construct
+    pullbacks. -/
+def has_pullbacks_of_has_binary_products_of_has_equalizers
+  (C : Type u) [𝒞 : category.{v} C] [has_binary_products.{v} C] [has_equalizers.{v} C] :
+  has_pullbacks.{v} C :=
+has_pullbacks_of_has_limit_cospan C
+
+end
+
+/-- If the coproduct `Y ⨿ Z` and the coequalizer of `f ≫ ι₁` and `g ≫ ι₂` exist, then the
+    pushout of `f` and `g` exists: It is given by composing the inclusions with the coequalizer. -/
+def has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair
+  {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [has_colimit (pair Y Z)]
+  [has_colimit (parallel_pair (f ≫ coprod.inl) (g ≫ coprod.inr))] : has_colimit (span f g) :=
+let ι₁ : Y ⟶ Y ⨿ Z := coprod.inl, ι₂ : Z ⟶ Y ⨿ Z := coprod.inr,
+  c := coequalizer.π (f ≫ ι₁) (g ≫ ι₂) in
+{ cocone := pushout_cocone.mk (ι₁ ≫ c) (ι₂ ≫ c) $
+    by rw [←category.assoc, ←category.assoc, coequalizer.condition],
+  is_colimit := pushout_cocone.is_colimit.mk _
+    (λ s, coequalizer.desc (f ≫ ι₁) (g ≫ ι₂) (coprod.desc (s.ι.app walking_span.left)
+      (s.ι.app walking_span.right)) $ by
+        rw [category.assoc, colimit.ι_desc, category.assoc, colimit.ι_desc];
+        exact pushout_cocone.condition _)
+    (by simp) (by simp) $ λ s m h, by
+      ext; simp only [colimit.ι_desc, cofork.of_π_app_one]; rw [←category.assoc];
+      exact walking_pair.cases_on j (h walking_span.left) (h walking_span.right) }
+
+section
+
+local attribute [instance] has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair
+
+/-- If a category has all binary coproducts and all coequalizers, then it also has all pushouts.
+    As usual, this is not an instance, since there may be a more direct way to construct
+    pushouts. -/
+def has_pushouts_of_has_binary_coproducts_of_has_coequalizers
+  (C : Type u) [𝒞 : category.{v} C] [has_binary_coproducts.{v} C] [has_coequalizers.{v} C] :
+  has_pushouts.{v} C :=
+has_pushouts_of_has_colimit_span C
+
+end
+
+end category_theory.limits

src/category_theory/limits/shapes/pullbacks.lean

@@ -217,16 +217,18 @@ def mk {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : pu
   { app := λ j, walking_cospan.cases_on j fst snd (fst ≫ f),
     naturality' := λ j j' f, by cases f; obviously } }
 
+@[simp] lemma mk_π_app_left {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
+  (mk fst snd eq).π.app left = fst := rfl
+@[simp] lemma mk_π_app_right {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
+  (mk fst snd eq).π.app right = snd := rfl
+@[simp] lemma mk_π_app_one {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
+  (mk fst snd eq).π.app one = fst ≫ f := rfl
+
 @[reassoc] lemma condition (t : pullback_cone f g) : fst t ≫ f = snd t ≫ g :=
 begin
   erw [t.w inl, ← t.w inr], refl
 end
 
-@[simp] lemma mk_left {L : C} {lx : L ⟶ X} {ly : L ⟶ Y} {e : lx ≫ f = ly ≫ g} :
-  (pullback_cone.mk lx ly e).π.app left = lx := rfl
-@[simp] lemma mk_right {L : C} {lx : L ⟶ X} {ly : L ⟶ Y} {e : lx ≫ f = ly ≫ g} :
-  (pullback_cone.mk lx ly e).π.app right = ly := rfl
-
 /-- To check whether a morphism is equalized by the maps of a pullback cone, it suffices to check
   it for `fst t` and `snd t` -/
 lemma equalizer_ext (t : pullback_cone f g) {W : C} {k l : W ⟶ t.X}
@@ -239,6 +241,19 @@ lemma equalizer_ext (t : pullback_cone f g) {W : C} {k l : W ⟶ t.X}
     ... = l ≫ t.π.app left ≫ (cospan f g).map inl : by rw [←category.assoc, h₀, category.assoc]
     ... = l ≫ t.π.app one : by rw t.w
 
+/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
+    only asks for a proof of facts that carry any mathematical content -/
+def is_limit.mk (t : pullback_cone f g) (lift : Π (s : cone (cospan f g)), s.X ⟶ t.X)
+  (fac_left : ∀ (s : cone (cospan f g)), lift s ≫ t.π.app left = s.π.app left)
+  (fac_right : ∀ (s : cone (cospan f g)), lift s ≫ t.π.app right = s.π.app right)
+  (uniq : ∀ (s : cone (cospan f g)) (m : s.X ⟶ t.X)
+    (w : ∀ j : walking_cospan, m ≫ t.π.app j = s.π.app j), m = lift s) :
+  is_limit t :=
+{ lift := lift,
+  fac' := λ s j, walking_cospan.cases_on j (fac_left s) (fac_right s) $
+    by rw [←t.w inl, ←s.w inl, ←fac_left s, category.assoc],
+  uniq' := uniq }
+
 end pullback_cone
 
 abbreviation pushout_cocone (f : X ⟶ Y) (g : X ⟶ Z) := cocone (span f g)
@@ -256,6 +271,13 @@ def mk {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : pu
   { app := λ j, walking_span.cases_on j (f ≫ inl) inl inr,
     naturality' := λ j j' f, by cases f; obviously } }
 
+@[simp] lemma mk_ι_app_left {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
+  (mk inl inr eq).ι.app left = inl := rfl
+@[simp] lemma mk_ι_app_right {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
+  (mk inl inr eq).ι.app right = inr := rfl
+@[simp] lemma mk_ι_app_zero {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
+  (mk inl inr eq).ι.app zero = f ≫ inl := rfl
+
 @[reassoc] lemma condition (t : pushout_cocone f g) : f ≫ (inl t) = g ≫ (inr t) :=
 begin
   erw [t.w fst, ← t.w snd], refl
@@ -273,6 +295,19 @@ lemma coequalizer_ext (t : pushout_cocone f g) {W : C} {k l : t.X ⟶ W}
     ... = ((span f g).map fst ≫ t.ι.app left) ≫ l : by rw [category.assoc, h₀, ←category.assoc]
     ... = t.ι.app zero ≫ l : by rw t.w
 
+/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
+    It only asks for a proof of facts that carry any mathematical content -/
+def is_colimit.mk (t : pushout_cocone f g) (desc : Π (s : cocone (span f g)), t.X ⟶ s.X)
+  (fac_left : ∀ (s : cocone (span f g)), t.ι.app left ≫ desc s = s.ι.app left)
+  (fac_right : ∀ (s : cocone (span f g)), t.ι.app right ≫ desc s = s.ι.app right)
+  (uniq : ∀ (s : cocone (span f g)) (m : t.X ⟶ s.X)
+    (w : ∀ j : walking_span, t.ι.app j ≫ m = s.ι.app j), m = desc s) :
+  is_colimit t :=
+{ desc := desc,
+  fac' := λ s j, walking_span.cases_on j (by rw [←s.w fst, ←t.w fst, category.assoc, fac_left s])
+    (fac_left s) (fac_right s),
+  uniq' := uniq }
+
 end pushout_cocone
 
 def cone.of_pullback_cone