feat(category_theory/limits): yoneda preserves limits (#5439)

yoneda and coyoneda preserve limits
leanprover-community · Dec 21, 2020 · c98d5bb · c98d5bb
1 parent 4778e16
commit c98d5bb
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 3 deletions.
diff --git a/src/category_theory/limits/preserves/limits.lean b/src/category_theory/limits/preserves/limits.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.limits.preserves.basic
-import category_theory.limits.shapes
 
 /-!
 # Isomorphisms about functors which preserve (co)limits

diff --git a/src/category_theory/limits/yoneda.lean b/src/category_theory/limits/yoneda.lean
@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.limits.limits
+import category_theory.limits.functor_category
 
 /-!
 # The colimit of `coyoneda.obj X` is `punit`
@@ -18,11 +19,11 @@ open category_theory
 open category_theory.limits
 
 universes v u
-variables {C : Type v} [small_category.{v} C]
 
 namespace category_theory
 
 namespace coyoneda
+variables {C : Type v} [small_category.{v} C]
 
 /--
 The colimit cocone over `coyoneda.obj X`, with cocone point `punit`.
@@ -53,4 +54,36 @@ colimit.iso_colimit_cocone { cocone := _, is_colimit := colimit_cocone_is_colimi
 
 end coyoneda
 
+variables {C : Type u} [category.{v} C]
+
+open limits
+
+/-- The yoneda embedding `yoneda.obj X : Cᵒᵖ ⥤ Type v` for `X : C` preserves limits. -/
+instance yoneda_preserves_limits (X : C) : preserves_limits (yoneda.obj X) :=
+{ preserves_limits_of_shape := λ J 𝒥, by exactI
+  { preserves_limit := λ K,
+    { preserves := λ c t,
+      { lift := λ s x, has_hom.hom.unop (t.lift ⟨op X, λ j, (s.π.app j x).op, λ j₁ j₂ α, _⟩),
+        fac' := λ s j, funext $ λ x, has_hom.hom.op_inj (t.fac _ _),
+        uniq' := λ s m w, funext $ λ x,
+        begin
+          refine has_hom.hom.op_inj (t.uniq ⟨op X, _, _⟩ _ (λ j, _)),
+          { dsimp, simp [← s.w α] }, -- See library note [dsimp, simp]
+          { exact has_hom.hom.unop_inj (congr_fun (w j) x) },
+        end } } } }
+
+/-- The coyoneda embedding `coyoneda.obj X : C ⥤ Type v` for `X : Cᵒᵖ` preserves limits. -/
+instance coyoneda_preserves_limits (X : Cᵒᵖ) : preserves_limits (coyoneda.obj X) :=
+{ preserves_limits_of_shape := λ J 𝒥, by exactI
+  { preserves_limit := λ K,
+    { preserves := λ c t,
+      { lift := λ s x, t.lift ⟨unop X, λ j, s.π.app j x, λ j₁ j₂ α, by { dsimp, simp [← s.w α]}⟩,
+          -- See library note [dsimp, simp]
+        fac' := λ s j, funext $ λ x, t.fac _ _,
+        uniq' := λ s m w, funext $ λ x,
+        begin
+          refine (t.uniq ⟨unop X, _⟩ _ (λ j, _)),
+          exact congr_fun (w j) x,
+        end } } } }
+
 end category_theory