Zulip Chat Archive

Stream: maths

Topic: Why small diagrams?


view this post on Zulip Ken Lee (Dec 20 2020 at 17:08):

If I'm not mistaken, in mathlib the definition of a limit of a diagram F:JCF : J \to C requires JJ to be small and in the same universe as morphisms in CC. Why is this?

view this post on Zulip Adam Topaz (Dec 20 2020 at 17:30):

I think this is probably because of what the universal property of the limit says.

view this post on Zulip Reid Barton (Dec 20 2020 at 17:36):

I think it was more a precaution to avoid unnecessary complexity than anything else

view this post on Zulip Reid Barton (Dec 20 2020 at 17:40):

At some point you'll be forced into this choice because they are typically the limits that exist, but perhaps the definition of is_limit itself (for instance) doesn't need it

view this post on Zulip Kenny Lau (Dec 20 2020 at 19:11):

@Ken Lee Because the product of copies of Z : Type 0 indexed over Type 1 doesn't live in Type 0 anymore

view this post on Zulip Kenny Lau (Dec 20 2020 at 19:11):

It's too big

view this post on Zulip Ken Lee (Dec 20 2020 at 19:13):

"too big" in terms of objects?

view this post on Zulip Kenny Lau (Dec 20 2020 at 19:14):

yeah

view this post on Zulip Ken Lee (Dec 20 2020 at 19:15):

but then in the definition of limits, JJ is in the same universe as morphisms of CC, not objects? perhaps I'm reading it wrong...

view this post on Zulip Ken Lee (Dec 20 2020 at 19:16):

also, I don't see how your example addresses why the shape JJ of the diagram needs to be small

view this post on Zulip Reid Barton (Dec 20 2020 at 19:19):

The morphisms of Type 0 belong to Type 0, and that's also the size of colimits/limits that Type 0 is closed under. The objects of Type 0 belong to Type 1 and that's too big.

view this post on Zulip Kenny Lau (Dec 20 2020 at 19:22):

@Ken Lee Type 1 is the diagram (the discrete category)

view this post on Zulip Reid Barton (Dec 20 2020 at 19:23):

Even the product over Type 0 doesn't live in Type 0


Last updated: May 09 2021 at 10:11 UTC