LKE along Yoneda preserves colimits and universes

Stream: mathlib4

[Robin Carlier]

The file file#Mathlib/CategoryTheory/Limits/Presheaf contains docs#CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff, but the universes levels in this theorem feel restrictive: if we’re taking a Type v₁-valued Yoneda, then the target category ℰ is assumed to have v₁-small hom sets. I always thought that this theorem holds regardless of the target category, as long as it has the relevant colimits for building the Kan extension (e.g any category with v₁-small colimits should be enough).

It seems I can trace it back to the fact that preservation of colimits for the left Kan extension is proven through docs#CategoryTheory.Presheaf.yonedaAdjunction, which assumes the same size constraint, but it does not seems super straightforward to change it (the constructrution of restrictedYoneda requires it). But maybe there is an alternative proof that the left extensions preserves colimits that does not assume this?

The converse (preserves colimits -> left Kan extended) seems to generalize smoothly to larger universes.

cc @Joël Riou, who’s responsible for the latest version of there theorems according to git blame.

[Robin Carlier]

For context: given a v₁-cocomplete category V and v : V, the "v₁-copower of v" functor Type v₁ ⥤ V should be characterized as the essentially unique functor that preserves colimits and that sends the terminal object to v, and It'd be nice if the machinery of file#Mathlib/CategoryTheory/Limits/Presheaf could apply.

[Joël Riou]

I am working on removing these universe restrictions, which also impact the definition of singular homology #mathlib4 > Singular homology and universes @ 💬

[Robin Carlier]

Great! I’ll see if I can make the unit of Day convolution work around this in the meantime (this is where I need copowers).