Zulip Chat Archive

Stream: maths

Topic: Why small diagrams?

Ken Lee (Dec 20 2020 at 17:08):

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

Adam Topaz (Dec 20 2020 at 17:30):

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

Reid Barton (Dec 20 2020 at 17:36):

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

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

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

Kenny Lau (Dec 20 2020 at 19:11):

It's too big

Ken Lee (Dec 20 2020 at 19:13):

"too big" in terms of objects?

Kenny Lau (Dec 20 2020 at 19:14):

yeah

Ken Lee (Dec 20 2020 at 19:15):

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

Ken Lee (Dec 20 2020 at 19:16):

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

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.

Kenny Lau (Dec 20 2020 at 19:22):

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

Reid Barton (Dec 20 2020 at 19:23):

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

Last updated: Dec 20 2023 at 11:08 UTC