feat(category_theory/limits): construct equalizers from pullbacks and products (#2124)

* construct equalizers from pullbacks and products

* ...

* changes from review

* Add docstrings

* golf proofs a little

* linter

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

Author: 3 people

src/category_theory/category/default.lean

@@ -90,6 +90,16 @@ section
 variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
 include 𝒞
 
+/-- postcompose an equation between morphisms by another morphism -/
+lemma eq_whisker {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : f ≫ h = g ≫ h :=
+by rw w
+/-- precompose an equation between morphisms by another morphism -/
+lemma whisker_eq (f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h :=
+by rw w
+
+infixr ` =≫ `:80 := eq_whisker
+infixr ` ≫= `:80 := whisker_eq
+
 lemma eq_of_comp_left_eq {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) : f = g :=
 by { convert w (𝟙 Y), tidy }
 lemma eq_of_comp_right_eq {f g : Y ⟶ Z} (w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) : f = g :=

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

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2020 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+
+import category_theory.limits.shapes.equalizers
+import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.pullbacks
+
+/-!
+# Constructing equalizers from pullbacks and binary products.
+
+If a category has pullbacks and binary products, then it has equalizers.
+
+TODO: provide the dual result.
+-/
+universes v u
+
+open category_theory category_theory.category
+
+namespace category_theory.limits
+
+variables {C : Type u} [𝒞 : category.{v} C] [has_binary_products.{v} C] [has_pullbacks.{v} C]
+include 𝒞
+
+-- We hide the "implementation details" inside a namespace
+namespace has_equalizers_of_pullbacks_and_binary_products
+
+/-- Define the equalizing object -/
+@[reducible]
+def construct_equalizer (F : walking_parallel_pair ⥤ C) : C :=
+pullback (prod.lift (𝟙 _) (F.map walking_parallel_pair_hom.left))
+         (prod.lift (𝟙 _) (F.map walking_parallel_pair_hom.right))
+
+/-- Define the equalizing morphism -/
+abbreviation pullback_fst (F : walking_parallel_pair ⥤ C) :
+  construct_equalizer F ⟶ F.obj walking_parallel_pair.zero :=
+pullback.fst
+
+lemma pullback_fst_eq_pullback_snd (F : walking_parallel_pair ⥤ C) :
+  pullback_fst F = pullback.snd :=
+by convert pullback.condition =≫ limits.prod.fst; simp
+
+/-- Define the equalizing cone -/
+@[reducible]
+def equalizer_cone (F : walking_parallel_pair ⥤ C) : cone F :=
+cone.of_fork
+  (fork.of_ι (pullback_fst F)
+    (begin
+      conv_rhs { rw pullback_fst_eq_pullback_snd, },
+      convert pullback.condition =≫ limits.prod.snd using 1; simp
+     end))
+
+/-- Show the equalizing cone is a limit -/
+def equalizer_cone_is_limit (F : walking_parallel_pair ⥤ C) : is_limit (equalizer_cone F) :=
+{ lift :=
+  begin
+    intro c, apply pullback.lift (c.π.app _) (c.π.app _),
+    apply limit.hom_ext,
+    rintro (_ | _); simp
+  end,
+  fac' :=
+  begin
+    rintros c (_ | _),
+    { simp, refl },
+    { simp, exact c.w _ }
+  end,
+  uniq' :=
+  begin
+    intros c _ J,
+    have J0 := J walking_parallel_pair.zero, simp at J0,
+    apply pullback.hom_ext,
+    { rwa limit.lift_π },
+    { erw [limit.lift_π, ← J0, pullback_fst_eq_pullback_snd] }
+  end }
+
+end has_equalizers_of_pullbacks_and_binary_products
+
+open has_equalizers_of_pullbacks_and_binary_products
+/-- Any category with pullbacks and binary products, has equalizers. -/
+-- This is not an instance, as it is not always how one wants to construct equalizers!
+def has_equalizers_of_pullbacks_and_binary_products :
+  has_equalizers.{v} C :=
+{ has_limits_of_shape :=
+  { has_limit := λ F,
+    { cone := equalizer_cone F,
+      is_limit := equalizer_cone_is_limit F } } }
+
+end category_theory.limits