Zulip Chat Archive

Stream: Is there code for X?

Topic: Presheaves have all (co)limits


view this post on Zulip Adam Topaz (Dec 07 2020 at 16:54):

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?

view this post on Zulip Johan Commelin (Dec 07 2020 at 17:09):

@Bhavik Mehta :up:

view this post on Zulip Reid Barton (Dec 07 2020 at 17:11):

It's definitely somewhere

view this post on Zulip Reid Barton (Dec 07 2020 at 17:12):

for diagrams in any (co)complete category

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:12):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:14):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:14):

Got it!

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:14):

import category_theory.limits.functor_category was missing.

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:15):

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

view this post on Zulip Bhavik Mehta (Dec 07 2020 at 17:20):

Yup as Reid says this is in mathlib

view this post on Zulip Bhavik Mehta (Dec 07 2020 at 17:20):

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

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:25):

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?

view this post on Zulip Bhavik Mehta (Dec 07 2020 at 17:29):

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


Last updated: May 17 2021 at 16:26 UTC