Zulip Chat Archive

Stream: maths

Topic: closure under colimits


view this post on Zulip Reid Barton (Dec 08 2018 at 05:53):

Suppose C is a category.{u v} that has_colimits and I have a family A_i of objects of C indexed by a Type v. I also have (let's say for simplicity) a fixed J which is a small_category.{v}. I want to construct the closure of the objects A_i under colimits of shape J, as a new family also indexed on a Type v. Is it possible?

view this post on Zulip Reid Barton (Dec 08 2018 at 05:58):

I was going to use an inductive type of course, but in order to write down the data needed in the inductive constructor, I also need to know what the actual objects in C are (that is, the values of the indexed family), because a diagram involves morphisms in C between those objects. So I end up with an inductive-recursive definition.

view this post on Zulip Reid Barton (Dec 08 2018 at 06:00):

I thought about adding the value of the object as an index of the type, but then it won't live in the right universe.

view this post on Zulip Reid Barton (Dec 08 2018 at 06:04):

The only thing I can think of is to do some manual transfinite recursion up to an ordinal of large enough cofinality (I know... that's my solution to everything).


Last updated: May 18 2021 at 08:14 UTC