Nuances regarding naturality

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Reid Barton]

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]

Another formulation is nonempty a -> trunc a, yes

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

choice, then trunc.mk

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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

[Kenny Lau]

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

[Bryan Gin-ge Chen]

How are you given V?

[Kenny Lau]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Kenny Lau]

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)