Zulip Chat Archive

Stream: maths

Topic: finite prods from binary prods


view this post on Zulip Kevin Buzzard (Dec 07 2019 at 15:48):

To prove that if a category has a terminal object and binary products then it has all finite products, it would be natural to first prove that if it has binary products and all limits of shapes J1 and J2, then it has all limits of shape J1 disjoint-union J2. Is this in mathlib? I couldn't even find the disjoint union construction, but I'm only just beginning to find my way around the library.

view this post on Zulip Johan Commelin (Dec 07 2019 at 15:59):

I think your first sentence is in mathlib

view this post on Zulip Johan Commelin (Dec 07 2019 at 15:59):

@Scott Morrison did that a while ago, I think

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 16:21):

Calle was trying to learn the category theory library by setting himself basic questions like this. I think it's a pretty neat idea.

view this post on Zulip Scott Morrison (Dec 07 2019 at 23:23):

No, this isn't done in mathlib. There's just a stub at src/category_theory/limits/shapes/constructions/finite_products.lean.


Last updated: May 18 2021 at 07:19 UTC