Zulip Chat Archive

Stream: general

Topic: definition depending on theorem


view this post on Zulip Johan Commelin (Oct 08 2018 at 06:30):

For my Lean-talk I would like a good example of a definition that depends on a (non-trivial) theorem. I don't want to use perfectoid spaces because that is way too advanced. I want to use this thread to collect a list of cute examples.

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2018 at 06:34):

How about: the dimension of a vector space depending on the fact that all bases have the same cardinality

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:43):

technically, the definition doesn't need this assumption, because it is defined as the minimum of such cardinalities. Instead, a proof is required to show that a minimum of cardinalities is well defined

view this post on Zulip Chris Hughes (Oct 08 2018 at 07:04):

convergence of exponential series. Also proof that the polynomial division algorithm is well founded took me a while. All of these can be done without any proofs technically, with some dite statement.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:06):

at the expense of computability of course

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 08:10):

The definition of an affine scheme needs the fact that the structure sheaf on Spec(A)Spec(A) is actually a sheaf, which took us quite some time to prove.

view this post on Zulip Johan Commelin (Oct 08 2018 at 08:10):

Yes, but I will be talking to an audience that partly doesn't know what a sheaf is...

view this post on Zulip Patrick Massot (Oct 08 2018 at 08:28):

What about the definition of addition of real numbers? Or even addition or integers


Last updated: May 08 2021 at 18:17 UTC