# Zulip Chat Archive

## Stream: maths

### Topic: Nuances regarding naturality

#### 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.

#### 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?

#### 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?

#### 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.

#### 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.

#### 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.

#### 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.

#### Reid Barton (Oct 05 2018 at 18:39):

Another formulation is `nonempty a -> trunc a`

, yes

#### 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.

#### 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

#### 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.

#### Reid Barton (Oct 05 2018 at 19:00):

`choice`

, then `trunc.mk`

#### 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.

#### Reid Barton (Oct 05 2018 at 19:04):

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

#### 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

#### 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".

#### Reid Barton (Oct 05 2018 at 19:06):

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

#### Kenny Lau (Oct 05 2018 at 19:10):

is it possible to define `trunc (basis V)`

computably?

#### Bryan Gin-ge Chen (Oct 05 2018 at 19:11):

How are you given `V`

?

#### Kenny Lau (Oct 05 2018 at 19:12):

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

#### 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.

#### 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.

#### 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