feat(algebraic_topology/simplicial_object + ...): Add has_limits + has_colimits instances (#6695)

This PR adds `has_limits` and `has_colimits` instances for the category of simplicial objects (assuming the existence of such an instance for the base category). The category of simplicial sets now has both limits and colimits, and we include a small example of a simplicial set (the circle) constructed as a colimit.

This PR also includes the following two components, which were required for the above:

1. A basic API for working with `ulift C` where `C` is a category. This was required to avoid some annoying universe issues in the definitions of `has_colimits` and `has_limits`.
2. A small shim that transports a `has_(co)limit` instance along an equivalence of categories.




Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>

Author: adamtopaz

src/algebraic_topology/simplicial_object.lean

@@ -4,6 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison
 -/
 import algebraic_topology.simplex_category
+import category_theory.category.ulift
+import category_theory.limits.functor_category
+import category_theory.opposites
+import category_theory.adjunction.limits
 
 /-!
 # Simplicial objects in a category.
@@ -13,6 +17,7 @@ A simplicial object in a category `C` is a `C`-valued presheaf on `simplex_categ
 
 open opposite
 open category_theory
+open category_theory.limits
 
 universes v u
 
@@ -26,6 +31,23 @@ This is the category of contravariant functors from `simplex_category` to `C`. -
 def simplicial_object := simplex_categoryᵒᵖ ⥤ C
 
 namespace simplicial_object
+
+instance {J : Type v} [small_category J] [has_limits_of_shape J C] :
+  has_limits_of_shape J (simplicial_object C) :=
+let E : (simplex_categoryᵒᵖ ⥤ C) ≌ (ulift.{v} simplex_category)ᵒᵖ ⥤ C :=
+  ulift.equivalence.op.congr_left in
+  adjunction.has_limits_of_shape_of_equivalence E.functor
+
+instance [has_limits C] : has_limits (simplicial_object C) := ⟨infer_instance⟩
+
+instance {J : Type v} [small_category J] [has_colimits_of_shape J C] :
+  has_colimits_of_shape J (simplicial_object C) :=
+let E : (simplex_categoryᵒᵖ ⥤ C) ≌ (ulift.{v} simplex_category)ᵒᵖ ⥤ C :=
+  ulift.equivalence.op.congr_left in
+  adjunction.has_colimits_of_shape_of_equivalence E.functor
+
+instance [has_colimits C] : has_colimits (simplicial_object C) := ⟨infer_instance⟩
+
 variables {C} (X : simplicial_object C)
 
 /-- Face maps for a simplicial object. -/

src/algebraic_topology/simplicial_set.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin, Scott Morrison
 -/
 import algebraic_topology.simplicial_object
 import category_theory.yoneda
+import category_theory.limits.types
 
 /-!
 A simplicial set is just a simplicial object in `Type`,
@@ -33,7 +34,7 @@ open category_theory
 /-- The category of simplicial sets.
 This is the category of contravariant functors from
 `simplex_category` to `Type u`. -/
-@[derive large_category]
+@[derive [large_category, limits.has_limits, limits.has_colimits]]
 def sSet : Type (u+1) := simplicial_object (Type u)
 
 namespace sSet
@@ -42,7 +43,7 @@ namespace sSet
 is the Yoneda embedding of `n`. -/
 def standard_simplex : simplex_category ⥤ sSet := yoneda
 
-localized "notation `Δ[`n`]` := standard_simplex.obj n" in sSet
+localized "notation `Δ[`n`]` := standard_simplex.obj (n : ℕ)" in sSet
 
 instance : inhabited sSet := ⟨standard_simplex.obj (0 : ℕ)⟩
 
@@ -82,11 +83,23 @@ def horn (n : ℕ) (i : fin (n+1)) : sSet :=
     exact set.range_comp_subset_range _ _ hj,
   end⟩ }
 
-localized "notation `Λ[`n`, `i`]` := horn n i" in sSet
+localized "notation `Λ[`n`, `i`]` := horn (n : ℕ) i" in sSet
 
 /-- The inclusion of the `i`-th horn of the `n`-th standard simplex into that standard simplex. -/
 def horn_inclusion (n : ℕ) (i : fin (n+1)) :
   Λ[n, i] ⟶ Δ[n] :=
 { app := λ m (α : {α : Δ[n].obj m // _}), α }
 
+section examples
+
+open_locale sSet
+
+/-- The simplicial circle. -/
+noncomputable def S1 : sSet :=
+limits.colimit $ limits.parallel_pair
+  ((standard_simplex.map $ simplex_category.δ 0) : Δ[0] ⟶ Δ[1])
+  (standard_simplex.map $ simplex_category.δ 1)
+
+end examples
+
 end sSet

src/category_theory/adjunction/limits.lean

@@ -115,6 +115,16 @@ lemma has_colimit_of_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_coli
 (@adjunction.has_colimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
 ((functor.right_unitor _).symm ≪≫ iso_whisker_left K (E.as_equivalence.unit_iso))
 
+/-- Transport a `has_colimits_of_shape` instance across an equivalence. -/
+lemma has_colimits_of_shape_of_equivalence (E : C ⥤ D) [is_equivalence E]
+  [has_colimits_of_shape J D] : has_colimits_of_shape J C :=
+⟨λ F, by exactI has_colimit_of_comp_equivalence F E⟩
+
+/-- Transport a `has_colimits` instance across an equivalence. -/
+lemma has_colimits_of_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimits D] :
+  has_colimits C :=
+⟨λ J hJ, by exactI has_colimits_of_shape_of_equivalence E⟩
+
 end preservation_colimits
 
 section preservation_limits
@@ -212,6 +222,15 @@ lemma has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit
 (@adjunction.has_limit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
 ((iso_whisker_left K E.as_equivalence.unit_iso.symm) ≪≫ (functor.right_unitor _))
 
+/-- Transport a `has_limits_of_shape` instance across an equivalence. -/
+lemma has_limits_of_shape_of_equivalence (E : D ⥤ C) [is_equivalence E] [has_limits_of_shape J C] :
+  has_limits_of_shape J D :=
+⟨λ F, by exactI has_limit_of_comp_equivalence F E⟩
+
+/-- Transport a `has_limits` instance across an equivalence. -/
+lemma has_limits_of_equivalence (E : D ⥤ C) [is_equivalence E] [has_limits C] : has_limits D :=
+⟨λ J hJ, by exactI has_limits_of_shape_of_equivalence E⟩
+
 end preservation_limits
 
 /-- auxiliary construction for `cocones_iso` -/

src/category_theory/category/ulift.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2021 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import category_theory.category
+import category_theory.equivalence
+
+/-!
+# Basic API for ulift
+
+This file contains a very basic API for working with the categorical 
+instance on `ulift C` where `C` is a type with a category instance.
+
+1. `category_theory.ulift.up` is the functorial version of the usual `ulift.up`. 
+2. `category_theory.ulift.down` is the functorial version of the usual `ulift.down`. 
+3. `category_theory.ulift.equivalence` is the categorical equivalence between 
+  `C` and `ulift C`.
+-/
+
+universes v u1 u2
+
+namespace category_theory
+
+variables {C : Type u1} [category.{v} C]
+
+/-- The functorial version of `ulift.up`. -/
+@[simps]
+def ulift.up : C ⥤ (ulift.{u2} C) :=
+{ obj := ulift.up,
+  map := λ X Y f, f }
+
+/-- The functorial version of `ulift.down`. -/
+@[simps]
+def ulift.down : (ulift.{u2} C) ⥤ C :=
+{ obj := ulift.down,
+  map := λ X Y f, f }
+
+/-- The categorical equivalence between `C` and `ulift C`. -/
+@[simps]
+def ulift.equivalence : C ≌ (ulift.{u2} C) :=
+{ functor := ulift.up,
+  inverse := ulift.down,
+  unit_iso :=
+  { hom := 𝟙 _,
+    inv := 𝟙 _ },
+  counit_iso :=
+  { hom :=
+    { app := λ X, 𝟙 _,
+      naturality' := λ X Y f, by {change f ≫ 𝟙 _ = 𝟙 _ ≫ f, simp} },
+    inv :=
+    { app := λ X, 𝟙 _,
+      naturality' := λ X Y f, by {change f ≫ 𝟙 _ = 𝟙 _ ≫ f, simp} },
+  hom_inv_id' := by {ext, change (𝟙 _) ≫ (𝟙 _) = 𝟙 _, simp},
+  inv_hom_id' := by {ext, change (𝟙 _) ≫ (𝟙 _) = 𝟙 _, simp} },
+  functor_unit_iso_comp' := λ X, by {change (𝟙 X) ≫ (𝟙 X) = 𝟙 X, simp} }
+
+end category_theory