refactor(CategoryTheory/Limits): generalize universes for colimits of representables (#27576)

Given a category `C` with `Category.{v₁} C`, this PR introduces a variant of the Yoneda embedding `uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type (max w v₁) ` which allows considering presheaves with values in higher universes.
The study of left Kan extensions along the Yoneda embedding is generalized using this variant. This allows to generalize the definition of the singular set of a simplicial set and the singular homology of a topological space to arbitrary universes.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -28,8 +28,7 @@ namespace SSet
 /-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the standard simplex `Δ[n]` is a
 cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
 Yoneda embedding). -/
-def stdSimplex : CosimplicialObject SSet.{u} :=
-  yoneda ⋙ uliftFunctor
+def stdSimplex : CosimplicialObject SSet.{u} := uliftYoneda
 
 @[inherit_doc SSet.stdSimplex]
 scoped[Simplicial] notation3 "Δ[" n "]" => SSet.stdSimplex.obj (SimplexCategory.mk n)
@@ -104,7 +103,7 @@ lemma map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : Sim
 /-- The canonical bijection `(stdSimplex.obj n ⟶ X) ≃ X.obj (op n)`. -/
 def _root_.SSet.yonedaEquiv {X : SSet.{u}} {n : SimplexCategory} :
     (stdSimplex.obj n ⟶ X) ≃ X.obj (op n) :=
-  yonedaCompUliftFunctorEquiv X n
+  uliftYonedaEquiv
 
 lemma yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) :
     yonedaEquiv.{u} (stdSimplex.map f) = objEquiv.symm f :=

Mathlib/AlgebraicTopology/SingularHomology/Basic.lean

@@ -18,35 +18,35 @@ noncomputable section
 
 namespace AlgebraicTopology
 
-open CategoryTheory
+open CategoryTheory Limits
 
 universe w v u
 
-variable (C : Type u) [Category.{v} C] [Limits.HasCoproducts.{0} C]
+variable (C : Type u) [Category.{v} C] [HasCoproducts.{w} C]
 variable [Preadditive C] [CategoryWithHomology C] (n : ℕ)
 
 /--
 The singular chain complex associated to a simplicial set, with coefficients in `X : C`.
 One can recover the ordinary singular chain complex when `C := Ab` and `X := ℤ`.
 -/
-def SSet.singularChainComplexFunctor [Limits.HasCoproducts.{w} C] :
+def SSet.singularChainComplexFunctor :
     C ⥤ SSet.{w} ⥤ ChainComplex C ℕ :=
   (Functor.postcompose₂.obj (AlgebraicTopology.alternatingFaceMapComplex _)).obj
-    (Limits.sigmaConst ⋙ SimplicialObject.whiskering _ _)
+    (sigmaConst ⋙ SimplicialObject.whiskering _ _)
 
 /-- The singular chain complex functor with coefficients in `C`. -/
 def singularChainComplexFunctor :
-    C ⥤ TopCat.{0} ⥤ ChainComplex C ℕ :=
-  SSet.singularChainComplexFunctor.{0} C ⋙ (Functor.whiskeringLeft _ _ _).obj TopCat.toSSet
+    C ⥤ TopCat.{w} ⥤ ChainComplex C ℕ :=
+  SSet.singularChainComplexFunctor.{w} C ⋙ (Functor.whiskeringLeft _ _ _).obj TopCat.toSSet.{w}
 
 /-- The `n`-th singular homology functor with coefficients in `C`. -/
-def singularHomologyFunctor : C ⥤ TopCat.{0} ⥤ C :=
+def singularHomologyFunctor : C ⥤ TopCat.{w} ⥤ C :=
   singularChainComplexFunctor C ⋙
     (Functor.whiskeringRight _ _ _).obj (HomologicalComplex.homologyFunctor _ _ n)
 
 section TotallyDisconnectedSpace
 
-variable (R : C) (X : TopCat.{0}) [TotallyDisconnectedSpace X]
+variable (R : C) (X : TopCat.{w}) [TotallyDisconnectedSpace X]
 
 /-- If `X` is totally disconnected,
 its singular chain complex is given by `R[X] ←0- R[X] ←𝟙- R[X] ←0- R[X] ⋯`,
@@ -61,23 +61,27 @@ def singularChainComplexFunctorIsoOfTotallyDisconnectedSpace :
     AlgebraicTopology.alternatingFaceMapComplexConst.app _
 
 omit [CategoryWithHomology C] in
-lemma singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace [Limits.HasZeroObject C]
+lemma singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace
     (hn : n ≠ 0) :
     (((singularChainComplexFunctor C).obj R).obj X).ExactAt n :=
+  have := hasCoproducts_shrink.{0, w} (C := C)
+  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
   .of_iso (ChainComplex.alternatingConst_exactAt _ _ hn)
     (singularChainComplexFunctorIsoOfTotallyDisconnectedSpace C R X).symm
 
 lemma isZero_singularHomologyFunctor_of_totallyDisconnectedSpace (hn : n ≠ 0) :
-    Limits.IsZero (((singularHomologyFunctor C n).obj R).obj X) :=
-  have : Limits.HasZeroObject C := ⟨_, Limits.initialIsInitial.isZero⟩
+    IsZero (((singularHomologyFunctor C n).obj R).obj X) :=
+  have := hasCoproducts_shrink.{0, w} (C := C)
+  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
   (singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace C n R X hn).isZero_homology
 
 /-- The zeroth singular homology of a totally disconnected space is the
 free `R`-module generated by elements of `X`. -/
 noncomputable
 def singularHomologyFunctorZeroOfTotallyDisconnectedSpace :
     ((singularHomologyFunctor C 0).obj R).obj X ≅ ∐ fun _ : X ↦ R :=
-  have : Limits.HasZeroObject C := ⟨_, Limits.initialIsInitial.isZero⟩
+  have := hasCoproducts_shrink.{0, w} (C := C)
+  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
   (HomologicalComplex.homologyFunctor _ _ 0).mapIso
       (singularChainComplexFunctorIsoOfTotallyDisconnectedSpace C R X) ≪≫
     ChainComplex.alternatingConstHomologyZero _

Mathlib/AlgebraicTopology/SingularSet.lean

@@ -3,16 +3,17 @@ Copyright (c) 2023 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kim Morrison, Adam Topaz
 -/
-import Mathlib.AlgebraicTopology.SimplicialSet.Basic
+import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.Topology.Category.TopCat.Limits.Basic
+import Mathlib.Topology.Category.TopCat.ULift
 
 /-!
 # The singular simplicial set of a topological space and geometric realization of a simplicial set
 
 The *singular simplicial set* `TopCat.toSSet.obj X` of a topological space `X`
-has as `n`-simplices the continuous maps `⦋n⦌.toTop → X`.
+has `n`-simplices which identify to continuous maps `⦋n⦌.toTop → X`.
 Here, `⦋n⦌.toTop` is the standard topological `n`-simplex,
 defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology.
 
@@ -27,52 +28,61 @@ It is the left Kan extension of `SimplexCategory.toTop` along the Yoneda embeddi
   assigning the geometric realization to a simplicial set.
 * `sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet` is the adjunction between these two functors.
 
-## TODO
+## TODO (@joelriou)
 
-- Generalize to an adjunction between `SSet.{u}` and `TopCat.{u}` for any universe `u`
 - Show that the singular simplicial set is a Kan complex.
-- Show the adjunction `sSetTopAdj` is a Quillen adjunction.
+- Show the adjunction `sSetTopAdj` is a Quillen equivalence.
 
 -/
 
+universe u
+
 open CategoryTheory
 
 /-- The functor associating the *singular simplicial set* to a topological space.
 
-Let `X` be a topological space.
+Let `X : TopCat.{u}` be a topological space.
 Then the singular simplicial set of `X`
-has as `n`-simplices the continuous maps `⦋n⦌.toTop → X`.
+has as `n`-simplices the continuous maps `ULift.{u} ⦋n⦌.toTop → X`.
 Here, `⦋n⦌.toTop` is the standard topological `n`-simplex,
 defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology. -/
-noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
-  Presheaf.restrictedYoneda SimplexCategory.toTop
+noncomputable def TopCat.toSSet : TopCat.{u} ⥤ SSet.{u} :=
+  Presheaf.restrictedULiftYoneda.{0} SimplexCategory.toTop.{u}
+
+/-- If `X : TopCat.{u}` and `n : SimplexCategoryᵒᵖ`,
+then `(toSSet.obj X).obj n` identifies to the type of continuous
+maps from the standard simplex `n.unop.toTopObj` to `X`. -/
+def TopCat.toSSetObjEquiv (X : TopCat.{u}) (n : SimplexCategoryᵒᵖ) :
+    (toSSet.obj X).obj n ≃ C(n.unop.toTopObj, X) :=
+  Equiv.ulift.{0}.trans (ConcreteCategory.homEquiv.trans
+    (Homeomorph.ulift.continuousMapCongr (.refl _)))
 
 /-- The *geometric realization functor* is
 the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
 
 It is left adjoint to `TopCat.toSSet`, as witnessed by `sSetTopAdj`. -/
-noncomputable def SSet.toTop : SSet ⥤ TopCat :=
-  yoneda.leftKanExtension SimplexCategory.toTop
+noncomputable def SSet.toTop : SSet.{u} ⥤ TopCat.{u} :=
+  stdSimplex.{u}.leftKanExtension SimplexCategory.toTop
 
 /-- Geometric realization is left adjoint to the singular simplicial set construction. -/
-noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
-  Presheaf.yonedaAdjunction (yoneda.leftKanExtension SimplexCategory.toTop)
-    (yoneda.leftKanExtensionUnit SimplexCategory.toTop)
+noncomputable def sSetTopAdj : SSet.toTop.{u} ⊣ TopCat.toSSet.{u} :=
+  Presheaf.uliftYonedaAdjunction
+    (SSet.stdSimplex.{u}.leftKanExtension SimplexCategory.toTop)
+    (SSet.stdSimplex.{u}.leftKanExtensionUnit SimplexCategory.toTop)
 
 /-- The geometric realization of the representable simplicial sets agree
   with the usual topological simplices. -/
 noncomputable def SSet.toTopSimplex :
-    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
-  Presheaf.isExtensionAlongYoneda _
+    SSet.stdSimplex.{u} ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
+  Presheaf.isExtensionAlongULiftYoneda _
+
+instance : SSet.toTop.{u}.IsLeftKanExtension SSet.toTopSimplex.inv :=
+  inferInstanceAs (Functor.IsLeftKanExtension _
+    (SSet.stdSimplex.{u}.leftKanExtensionUnit SimplexCategory.toTop.{u}))
 
 /-- The singular simplicial set of a totally disconnected space is the constant simplicial set. -/
-noncomputable
-def TopCat.toSSetIsoConst (X : TopCat) [TotallyDisconnectedSpace X] :
+noncomputable def TopCat.toSSetIsoConst (X : TopCat.{u}) [TotallyDisconnectedSpace X] :
     TopCat.toSSet.obj X ≅ (Functor.const _).obj X :=
-  .symm <|
-  NatIso.ofComponents (fun i ↦
-    { inv v := v.1 ⟨Pi.single 0 1, show ∑ _, _ = _ by simp⟩
-      hom x := TopCat.ofHom ⟨fun _ ↦ x, continuous_const⟩
-      inv_hom_id := types_ext _ _ fun f ↦ TopCat.hom_ext (ContinuousMap.ext
-        fun j ↦ TotallyDisconnectedSpace.eq_of_continuous (α := i.unop.toTopObj) _ f.1.2 _ _)
-      hom_inv_id := rfl }) (by intros; ext; rfl)
+  (NatIso.ofComponents (fun n ↦ Equiv.toIso
+    ((TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace _ X).symm.trans
+      (X.toSSetObjEquiv n).symm))).symm

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin, Adam Topaz
 -/
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.AlgebraicTopology.SimplexCategory.Basic
-import Mathlib.Topology.Category.TopCat.Basic
+import Mathlib.Topology.Category.TopCat.ULift
 import Mathlib.Topology.Connected.PathConnected
 
 /-!
@@ -16,6 +16,7 @@ topological `n`-simplex.
 This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
 -/
 
+universe u
 
 noncomputable section
 
@@ -97,9 +98,10 @@ theorem continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) : Continuous (
   dsimp only [coe_toTopMap]
   exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)
 
-/-- The functor associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`. -/
+/-- The functor `SimplexCategory ⥤ TopCat.{0}`
+associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`. -/
 @[simps obj map]
-def toTop : SimplexCategory ⥤ TopCat where
+def toTop₀ : SimplexCategory ⥤ TopCat.{0} where
   obj x := TopCat.of x.toTopObj
   map f := TopCat.ofHom ⟨toTopMap f, by fun_prop⟩
   map_id := by
@@ -117,4 +119,10 @@ def toTop : SimplexCategory ⥤ TopCat where
       · tauto
     · apply Set.pairwiseDisjoint_filter
 
+/-- The functor `SimplexCategory ⥤ TopCat.{u}`
+associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`. -/
+@[simps! obj map, pp_with_univ]
+def toTop : SimplexCategory ⥤ TopCat.{u} :=
+  toTop₀ ⋙ TopCat.uliftFunctor
+
 end SimplexCategory

Mathlib/CategoryTheory/Closed/Types.lean

@@ -47,7 +47,7 @@ instance {C : Type v₁} [SmallCategory C] : CartesianClosed (C ⥤ Type v₁) :
     (fun F => by
       haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance
       letI : PreservesColimits (tensorLeft F) := ⟨by infer_instance⟩
-      have := Presheaf.isLeftAdjoint_of_preservesColimits (tensorLeft F)
+      have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)
       exact Exponentiable.mk _ _ (Adjunction.ofIsLeftAdjoint (tensorLeft F)))
 
 -- TODO: once we have `MonoidalClosed` instances for functor categories into general monoidal

Mathlib/CategoryTheory/Elements.lean

@@ -266,6 +266,32 @@ def costructuredArrowYonedaEquivalenceInverseπ (F : Cᵒᵖ ⥤ Type v) :
     (costructuredArrowYonedaEquivalence F).inverse ⋙ (π F).leftOp ≅ CostructuredArrow.proj _ _ :=
   Iso.refl _
 
+/-- The opposite of the category of elements of a presheaf of types
+is equivalent to a category of costructured arrows for the Yoneda embedding functor. -/
+@[simps]
+def costructuredArrowULiftYonedaEquivalence (F : Cᵒᵖ ⥤ Type max w v) :
+    F.Elementsᵒᵖ ≌ CostructuredArrow uliftYoneda.{w} F where
+  functor :=
+    { obj x := CostructuredArrow.mk (uliftYonedaEquiv.{w}.symm x.unop.2)
+      map f := CostructuredArrow.homMk f.1.1.unop (by
+        dsimp
+        rw [← uliftYonedaEquiv_symm_map, map_snd]) }
+  inverse :=
+    { obj X := op (F.elementsMk _ (uliftYonedaEquiv.{w} X.hom))
+      map f := (homMk _ _ f.left.op (by
+        dsimp
+        rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op])).op }
+  unitIso := NatIso.ofComponents (fun x ↦ Iso.op (isoMk _ _ (Iso.refl _) (by simp)))
+    (fun f ↦ Quiver.Hom.unop_inj (by aesop))
+  counitIso := NatIso.ofComponents (fun X ↦ CostructuredArrow.isoMk (Iso.refl _))
+
+/-- The equivalence of categories `costructuredArrowULiftYonedaEquivalence`
+commutes with the projections. -/
+def costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso (F : Cᵒᵖ ⥤ Type max w v) :
+    (costructuredArrowULiftYonedaEquivalence.{w} F).functor ⋙ CostructuredArrow.proj _ _ ≅
+      (π F).leftOp :=
+  Iso.refl _
+
 end CategoryOfElements
 
 namespace Functor

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

@@ -225,7 +225,15 @@ def isPointwiseLeftKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
 namespace IsPointwiseLeftKanExtensionAt
 
 variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y)
-  [HasColimit (CostructuredArrow.proj L Y ⋙ F)]
+
+@[reassoc]
+lemma comp_homEquiv_symm {Z : H}
+    (φ : CostructuredArrow.proj L Y ⋙ F ⟶ (Functor.const _).obj Z)
+    (g : CostructuredArrow L Y) :
+    E.hom.app g.left ≫ E.right.map g.hom ≫ h.homEquiv.symm φ = φ.app g := by
+  simpa using h.ι_app_homEquiv_symm φ g
+
+variable [HasColimit (CostructuredArrow.proj L Y ⋙ F)]
 
 /-- A pointwise left Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
 `colimit (CostructuredArrow.proj L Y ⋙ F)`. -/

Mathlib/CategoryTheory/Limits/IsLimit.lean

@@ -360,6 +360,17 @@ def homEquiv (h : IsLimit t) {W : C} : (W ⟶ t.pt) ≃ ((Functor.const J).obj W
   left_inv f := h.hom_ext (by simp)
   right_inv π := by cat_disch
 
+@[reassoc (attr := simp)]
+lemma homEquiv_symm_π_app (h : IsLimit t) {W : C}
+    (f : (const J).obj W ⟶ F) (j : J) :
+    h.homEquiv.symm f ≫ t.π.app j = f.app j := by
+  simp [homEquiv]
+
+lemma homEquiv_symm_naturality (h : IsLimit t) {W W' : C}
+    (f : (const J).obj W ⟶ F) (g : W' ⟶ W) :
+    h.homEquiv.symm ((Functor.const _).map g ≫ f) = g ≫ h.homEquiv.symm f :=
+  h.homEquiv.injective (by aesop)
+
 /-- The universal property of a limit cone: a map `W ⟶ X` is the same as
   a cone on `F` with cone point `W`. -/
 def homIso (h : IsLimit t) (W : C) : ULift.{u₁} (W ⟶ t.pt : Type v₃) ≅ (const J).obj W ⟶ F :=
@@ -827,6 +838,17 @@ def homEquiv (h : IsColimit t) {W : C} : (t.pt ⟶ W) ≃ (F ⟶ (const J).obj W
 lemma homEquiv_apply (h : IsColimit t) {W : C} (f : t.pt ⟶ W) :
     h.homEquiv f = (t.extend f).ι := rfl
 
+@[reassoc (attr := simp)]
+lemma ι_app_homEquiv_symm (h : IsColimit t) {W : C}
+    (f : F ⟶ (const J).obj W) (j : J) :
+    t.ι.app j ≫ h.homEquiv.symm f = f.app j := by
+  simp [homEquiv]
+
+lemma homEquiv_symm_naturality (h : IsColimit t) {W W' : C}
+    (f : F ⟶ (const J).obj W) (g : W ⟶ W') :
+    h.homEquiv.symm (f ≫ (Functor.const _).map g) = h.homEquiv.symm f ≫ g :=
+  h.homEquiv.injective (by aesop)
+
 /-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
   a cocone on `F` with cone point `W`. -/
 def homIso (h : IsColimit t) (W : C) : ULift.{u₁} (t.pt ⟶ W : Type v₃) ≅ F ⟶ (const J).obj W :=

Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean

@@ -6,8 +6,9 @@ Authors: Bhavik Mehta
 import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
-import Mathlib.CategoryTheory.Limits.Yoneda
+import Mathlib.CategoryTheory.Limits.Preserves.Ulift
 import Mathlib.CategoryTheory.Limits.Presheaf
+import Mathlib.CategoryTheory.Limits.Yoneda
 
 /-!
 # Preservation of (co)limits in the functor category
@@ -190,9 +191,10 @@ instance whiskeringRightPreservesColimits {C : Type*} [Category C] {D : Type*} [
 /-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`. -/
 lemma preservesLimit_of_lan_preservesLimit {C D : Type u} [SmallCategory C]
     [SmallCategory D] (F : C ⥤ D) (J : Type u) [SmallCategory J]
-    [PreservesLimitsOfShape J (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u)] : PreservesLimitsOfShape J F := by
-  apply @preservesLimitsOfShape_of_reflects_of_preserves _ _ _ _ _ _ _ _ F yoneda ?_
-  exact preservesLimitsOfShape_of_natIso (Presheaf.compYonedaIsoYonedaCompLan F).symm
+    [PreservesLimitsOfShape J (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u)] : PreservesLimitsOfShape J F :=
+  letI := preservesLimitsOfShape_of_natIso (J := J)
+    (Presheaf.compULiftYonedaIsoULiftYonedaCompLan.{u} F).symm
+  preservesLimitsOfShape_of_reflects_of_preserves F uliftYoneda.{u}
 
 /-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`. -/
 lemma preservesFiniteLimits_of_evaluation {D : Type*} [Category D] {E : Type*} [Category E]