## 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

It's too big

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

"too big" in terms of objects?

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: May 09 2021 at 10:11 UTC