From c240fcb38cfdbe15b790f8f62dae391e194277bd Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 16 Mar 2020 02:31:06 +0100 Subject: [PATCH] feat(category_theory/limits): pullbacks from binary products and equalizers (#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 Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- src/category_theory/limits/over.lean | 5 +- .../shapes/constructions/equalizers.lean | 2 +- .../shapes/constructions/pullbacks.lean | 87 ++++++++++++++++++- .../limits/shapes/pullbacks.lean | 45 ++++++++-- 4 files changed, 128 insertions(+), 11 deletions(-) diff --git a/src/category_theory/limits/over.lean b/src/category_theory/limits/over.lean index d87b7cfe5618b..25bb00f69f0b5 100644 --- a/src/category_theory/limits/over.lean +++ b/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, diff --git a/src/category_theory/limits/shapes/constructions/equalizers.lean b/src/category_theory/limits/shapes/constructions/equalizers.lean index 017f2a2660fb0..92718a285c228 100644 --- a/src/category_theory/limits/shapes/constructions/equalizers.lean +++ b/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, diff --git a/src/category_theory/limits/shapes/constructions/pullbacks.lean b/src/category_theory/limits/shapes/constructions/pullbacks.lean index e88969b13b76a..8fc14d8e8e980 100644 --- a/src/category_theory/limits/shapes/constructions/pullbacks.lean +++ b/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 diff --git a/src/category_theory/limits/shapes/pullbacks.lean b/src/category_theory/limits/shapes/pullbacks.lean index 0919f5288a00b..dd53585f78906 100644 --- a/src/category_theory/limits/shapes/pullbacks.lean +++ b/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