apply the density theorem in a larger universe?

Stream: mathlib4

[Emily Riehl]

I would like to apply the coYoneda lemma or density theorem to simplicial sets valued in an arbitrary universe. The following two haves fail unless I restrict my variable to be (X : SSet.{0}).

import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.CategoryTheory.Limits.Presheaf

namespace CategoryTheory

universe u

open Category Functor Limits Opposite SimplexCategory Simplicial SSet

def test (X : SSet.{u}) : Type := by
  have Xcolim := Presheaf.colimitOfRepresentable (C := SimplexCategory) X
  have Xcolim' := Presheaf.isColimitTautologicalCocone (C := SimplexCategory) X
  sorry

Can someone help me figure out how to fix this?

In case the setting is of interest, I opened up a PR #25010 will some challenges that I was hoping to entice someone to try to tackle. The result of closing the eight sorries is a theorem of interest to the infinity-cosmos project as I'll discuss in our synchronous meeting on Wednesday. More details about that meeting at the PR can be found in the infinity-cosmos channel (which I'd link to if I knew how to do that).

[Andrew Yang]

One option is to generalize the constructions of them, e.g. the following allows colimitOfRepresentable to take in a large presheaf.

import Mathlib.CategoryTheory.Elements

namespace CategoryTheory

open Category Limits

universe v₁ v₂ v₃ u₁ u₂ u₃

namespace Presheaf

variable {C : Type u₁} [Category.{v₁} C]

variable {ℰ : Type u₂} [Category.{v₁} ℰ] (A : C ⥤ ℰ)

/-- A functor to the presheaf category in which everything in the image is representable (witnessed
by the fact that it factors through the yoneda embedding).
`coconeOfRepresentable` gives a cocone for this functor which is a colimit and has point `P`.
-/
@[reducible]
def functorToRepresentables (P : Cᵒᵖ ⥤ Type max v₂ v₁) : P.Elementsᵒᵖ ⥤ Cᵒᵖ ⥤ Type max v₂ v₁ :=
  (CategoryOfElements.π P).leftOp ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor

/-- This is a cocone with point `P` for the functor `functorToRepresentables P`. It is shown in
`colimitOfRepresentable P` that this cocone is a colimit: that is, we have exhibited an arbitrary
presheaf `P` as a colimit of representables.

The construction of [MM92], Chapter I, Section 5, Corollary 3.
-/
@[simps]
noncomputable def coconeOfRepresentable (P : Cᵒᵖ ⥤ Type max v₂ v₁) :
    Cocone (functorToRepresentables P) where
  pt := P
  ι :=
    { app x := (yonedaCompUliftFunctorEquiv _ _).symm x.unop.2
      naturality := fun {x₁ x₂} f => by ext; simp [yonedaCompUliftFunctorEquiv] }

/-- The legs of the cocone `coconeOfRepresentable` are natural in the choice of presheaf. -/
theorem coconeOfRepresentable_naturality {P₁ P₂ : Cᵒᵖ ⥤ Type v₁} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) :
    (coconeOfRepresentable P₁).ι.app j ≫ α =
      (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j) := by
  ext T f
  simpa [coconeOfRepresentable_ι_app] using FunctorToTypes.naturality _ _ α f.down.op _

/-- The cocone with point `P` given by `coconeOfRepresentable` is a colimit:
that is, we have exhibited an arbitrary presheaf `P` as a colimit of representables.

The result of [MM92], Chapter I, Section 5, Corollary 3.
-/
noncomputable def colimitOfRepresentable (P : Cᵒᵖ ⥤ Type max v₂ v₁) :
    IsColimit (coconeOfRepresentable P) where
  desc s :=
    { app := fun X x => (s.ι.app (Opposite.op (Functor.elementsMk P X x))).app X (.up (𝟙 _))
      naturality := fun X Y f => by
        ext x
        have eq₁ := congr_fun (congr_app (s.w (CategoryOfElements.homMk (P.elementsMk X x)
          (P.elementsMk Y (P.map f x)) f rfl).op) Y) (.up (𝟙 _))
        dsimp at eq₁ ⊢
        simpa [← eq₁, id_comp] using
          congr_fun ((s.ι.app (Opposite.op (P.elementsMk X x))).naturality f) (.up (𝟙 _)) }
  fac s j := by
    ext X x
    let φ : j.unop ⟶ Functor.elementsMk P X
      (((yonedaCompUliftFunctorEquiv _ _).symm j.unop.2).app X x) := ⟨x.down.op, rfl⟩
    simpa using congr_fun (congr_app (s.ι.naturality φ.op).symm X) (.up (𝟙 _))
  uniq s m hm := by
    ext X x
    dsimp
    rw [← hm]
    apply congr_arg
    simp [coconeOfRepresentable_ι_app, yonedaCompUliftFunctorEquiv]

[Andrew Yang]

Another option is to apply it on

Presheaf.colimitOfRepresentable (C := ULiftHom SimplexCategory) (ULiftHom.down.op ⋙ X)

[Robin Carlier]

Potentially related: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LKE.20along.20Yoneda.20preserves.20colimits.20and.20universes

And https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LKE.20along.20Yoneda.20preserves.20colimits.20and.20universes (edit 8 hours later: wrong link... #mathlib4 > Singular homology and universes :man_facepalming: )

So the content of file#CategoryTheory/Limits/Presheaf has indeed universes restrictions and @Joël Riou is working on it.

[Emily Riehl]

Andrew Yang said:

Another option is to apply it on

Presheaf.colimitOfRepresentable (C := ULiftHom SimplexCategory) (ULiftHom.down.op ⋙ X)

Thanks I was trying to find this infrastructure on LeanSearch but failed. Now I'm trying to understand it.

In particular what is the let _ doing in the following:

def ULiftHom.{w,u} (C : Type u) : Type u :=
  let _ := ULift.{w} C
  C

It's clearly not necessary for this definition (of the type alias of the ULiftHom category) but if I comment it out everything below in this file breaks.

Edit: on closer inspection, it seems as if it's just forcing the second universe w to be a parameter in this definition.

[Robin Carlier]

Yes, this seems like a trick to "consume" the universe parameter w.

[Kevin Buzzard]

If you change it to ULift.{w} Nat does everything still compile?

[Robin Carlier]

Yes.