Zulip Chat Archive

Stream: maths

Topic: weird Lean proofs


view this post on Zulip Reid Barton (Nov 29 2018 at 01:36):

Lemma. If t:(Xj)jJXt : (X_j)_{j \in J} \to X is a colimit cocone in Set, then every element of XX is in the image of XjXX_j \to X for some jJj \in J.

Proof. Let f:XPropf : X \to \mathtt{Prop} be the function sending x to ∃ j y, t.ι.app j y = x and let gg be the constant function true. Then ff and gg agree after precomposition with each XjXX_j \to X, so they are equal.

view this post on Zulip Kenny Lau (Nov 29 2018 at 01:37):

you what

view this post on Zulip Keeley Hoek (Nov 29 2018 at 01:43):

To a category theorist, on a scale of 1-10, how old is the "I think it's actually called a 'ne'" joke

view this post on Zulip Kenny Lau (Nov 29 2018 at 01:45):

@Kevin Buzzard "lean will revolutionize mathematics"

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:24):

To a category theorist, on a scale of 1-10, how old is the "I think it's actually called a 'ne'" joke

I think that joke turned 10 several years ago...

view this post on Zulip Mario Carneiro (Nov 29 2018 at 05:29):

I don't see why this is a weird proof. Isn't this basically how you prove that epis are surjective in Set?

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:31):

We don't have Curry-Howard in mathematics, remember (-;

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:31):

So you can't even write this proof down in "mathematics"

view this post on Zulip Mario Carneiro (Nov 29 2018 at 05:32):

yes you can, just make f take values in {0, 1} or something, or do equality of sets instead (i.e. f denotes a subset of X)

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:36):

Sure... But I agree with Reid that is just feels a lot different then when you build a map to Prop.

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:36):

Anyway, it's probably just taste.

view this post on Zulip Mario Carneiro (Nov 29 2018 at 05:37):

I think that this is one of the really interesting places where you get a truly nonconstructive exists without choice

view this post on Zulip Chris Hughes (Dec 03 2018 at 19:03):

Can you prove the existence of a colimit cocone in Set without choice though?

view this post on Zulip Reid Barton (Dec 03 2018 at 19:06):

Yes (https://github.com/leanprover/mathlib/blob/master/category_theory/limits/types.lean#L49), and what I would consider the "normal" proof of the original fact consists of writing down this formula (which one has presumably done already), noting that the fact is obvious in this case, and using essential uniqueness of the colimit

view this post on Zulip Reid Barton (Dec 03 2018 at 19:12):

It might actually end up being easier in Lean than the one I outlined above, because I needed to do some juggling to get Prop into the correct universe to make that proof actually work

view this post on Zulip Reid Barton (Dec 03 2018 at 19:16):

You might be thinking of the situation where you have a type X and some subsets whose union is all of X, and you want to prove that X is some kind of colimit of the subsets


Last updated: May 06 2021 at 18:20 UTC