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.
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
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
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
Mario Carneiro (Oct 08 2018 at 07:06):
at the expense of computability of course
Kevin Buzzard (Oct 08 2018 at 08:10):
The definition of an affine scheme needs the fact that the structure sheaf on is actually a sheaf, which took us quite some time to prove.
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...
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