(Co)completion of a category

Stream: Is there code for X?

[Chris Hughes]

Do we have the universal property of the presheaf category as the cocompletion of a category. i.e. a cocontinuous functor $PSh(\mathcal{C}) \rightarrow \mathcal{D}$, given a functor $\mathcal{C} \rightarrow \mathcal{D}$ whenever $\mathcal{D}$ is cocomplete

[Johan Commelin]

cc @Bhavik Mehta

[Adam Topaz]

I do think we know that any presheaf is a colimit of representables. You could also use Kan extension along Yoneda to obtain the lift of a functor.

[Adam Topaz]

docs#category_theory.colimit_of_representable

[Adam Topaz]

Actually @Chris Hughes if you look at the rest of that file as well, it essentially has everything you need to view the category of presheaves as the free cocompletion.

[Chris Hughes]

Looks like it is this docs#category_theory.colimit_adj.extend_along_yoneda

[Chris Hughes]

Do we have the opposite version. Showing that $(\mathcal{C} \rightarrow Set)^{op}$ is the completion?

[Bhavik Mehta]

I don't think we do, it might be easy by duality or perhaps it's easier to just repeat and flip directions

[Reid Barton]

Presheaves being the free cocompletion is a specific and easy-to-write-down statement: for any cocomplete D, precomposition with the Yoneda embedding is an equivalence {colimit-preserving functors from presheaves on C to D} -> {all functors from C to D}. Do we have this statement? I didn't see it

[Adam Topaz]

Hmmm... do we have that docs#category_theory.colimit_adj.extend_along_yoneda preserves colimits? It seems we don't. That seems to be the only missing ingredient for the equivalence Reid mentioned. nevermind, we have it.

[Bhavik Mehta]

We don't have that specific statement, but the ingredients are all there