Zulip Chat Archive

Stream: maths

Topic: Nuances regarding naturality


view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:56):

https://mathoverflow.net/questions/244131/nuances-regarding-naturality?noredirect=1&lq=1

Does Lean have a good answer to this question? My understanding is that the OP is trying to define data which involves an uncomputable choice of some other data (and it's a theorem that such a choice can always be made in at least one way) and then a proof that the data we care about is independent of this uncomputable choice.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:05):

Is the function that sends a vector space to the cardinal corresponding to its dimension any "better" in any way than the function that sends a vector space to a basis which was chosen using the axiom of choice?

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 18:25):

Perhaps I'm missing something, but the dimension function is defined using the "choose-a-basis" function, right?

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 18:26):

I ran into this when I was working on the rank function for matroids (which is a generalization of dimension for f.d. vector spaces); even with unique existence, you still have to apply some form of choice to define the actual nat.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 18:37):

Yes. The question is whether the added nuance of the proof that the output is independent of the choice can be expressed in Lean. A mathematician might argue that they hadn't "seriously" used choice, or something. I was wondering if there was anything in this.

view this post on Zulip Chris Hughes (Oct 05 2018 at 18:38):

It could still be done computably, using trunc, instead of exists, and quot.lift instead of choice.

view this post on Zulip Reid Barton (Oct 05 2018 at 18:39):

The dimension function can be defined using only "unique choice" nonempty a -> (\all x y : a, x = y) -> a. This is just as noncomputable as full choice but philosophically less problematic (at least to me) because the type of the "unique choice" constant is a subsingleton.

view this post on Zulip Reid Barton (Oct 05 2018 at 18:39):

Another formulation is nonempty a -> trunc a, yes

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 18:40):

At the time I ended up throwing in an encodable instance. I'll have to look into trunc now that I know a little more about it though.

view this post on Zulip Reid Barton (Oct 05 2018 at 18:42):

The "pick a basis" function is different because its value depends on the interpretation of the choice constant

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 18:58):

What's nonempty a -> trunc a? I see nonempty_of_trunc in mathlib but not the other way around. Is this because in lean's foundations there's no unique choice? To define the dimension function in lean, am I right that you could only do it by returning the cardinality of "pick a basis"? Well-definedness would be proven and used separately I suppose.

view this post on Zulip Reid Barton (Oct 05 2018 at 19:00):

choice, then trunc.mk

view this post on Zulip Reid Barton (Oct 05 2018 at 19:03):

Lean's core library only has the axiom choice, and derives all the other classical principles from it. So in this setup you can't make fine distinctions between things like using choice and only using unique choice. However, you could imagine adding unique choice (and LEM) as separate axioms.

view this post on Zulip Reid Barton (Oct 05 2018 at 19:04):

You could also add the "axiom of choice" (which is a Prop) as a separate axiom.

view this post on Zulip Reid Barton (Oct 05 2018 at 19:05):

Then you could define the dimension function using only the "axiom of choice" (to prove nonempty (basis V)) and "unique choice" (to extract the dimension)--in order to do this you have to prove that every basis has the same cardinality

view this post on Zulip Reid Barton (Oct 05 2018 at 19:06):

Both of these axioms are subsingletons, so you can conclude that the dimension of a vector space doesn't depend on the interpretation of choice or on any other "arbitrary choices".

view this post on Zulip Reid Barton (Oct 05 2018 at 19:06):

You cannot define the "pick a basis" function this way

view this post on Zulip Kenny Lau (Oct 05 2018 at 19:10):

is it possible to define trunc (basis V) computably?

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 19:11):

How are you given V?

view this post on Zulip Kenny Lau (Oct 05 2018 at 19:12):

k : Type u
V : Type v
_inst_1 : field k
_inst_2 : vector_space k V

view this post on Zulip Chris Hughes (Oct 05 2018 at 19:13):

@Kenny Lau providing a truncated basis could be part of the definition of finite dimensional vector space.

view this post on Zulip Chris Hughes (Oct 05 2018 at 19:14):

For the infinite case you can't do it, but who cares when cardinals don't have decidable equality.

view this post on Zulip Kenny Lau (Oct 05 2018 at 19:14):

so essentially I'm asking for a term of the type \Pi (k : Type u) (V : Type v) [field k] [vector_space k V], trunc (basis k V)


Last updated: May 11 2021 at 15:12 UTC