Presheaves have all (co)limits

Stream: Is there code for X?

[Adam Topaz]

import category_theory.functor_category
import category_theory.limits.types

open category_theory
open category_theory.limits

variables (C : Type) [small_category C]

example : has_colimits (Cᵒᵖ ⥤ Type) := sorry -- Do we have this somewhere?
example : has_limits (Cᵒᵖ ⥤ Type) := sorry -- Do we have this somewhere?

[Johan Commelin]

@Bhavik Mehta :up:

[Reid Barton]

It's definitely somewhere

[Reid Barton]

for diagrams in any (co)complete category

[Adam Topaz]

Yeah, that's what I was expecting too, which is why the import category_theory.limits.types import is there

[Adam Topaz]

import category_theory.functor_category
import category_theory.limits.types
import category_theory.limits.functor_category

open category_theory
open category_theory.limits

variables (C : Type) [small_category C]

example : has_colimits (Cᵒᵖ ⥤ Type) := by apply_instance
example : has_limits (Cᵒᵖ ⥤ Type) := by apply_instance

[Adam Topaz]

Got it!

[Adam Topaz]

import category_theory.limits.functor_category was missing.

[Adam Topaz]

I don't presume the universal property of presheaves as being the free cocompletion is in mathlib?

[Bhavik Mehta]

Yup as Reid says this is in mathlib

[Bhavik Mehta]

@Adam Topaz It is, look in ct/limits/presheaf iirc

[Adam Topaz]

For a little context.... I'd like to define Ind C as the subcategory of Cᵒᵖ ⥤ Type generated by filtered colimits of representables. @Reid Barton @Bhavik Mehta Any thoughts on whether this is a good idea?

[Bhavik Mehta]

My instinct is that this might get awkward but I don't know for sure, and off the top of my head I don't have better suggestions. You probably want to use is_limit rather than isomorphisms with limit though if you do go about it this way