# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Classification of finite-dimensional vector spaces

#### Heather Macbeth (Jan 01 2021 at 16:02):

Do we have, there exists a linear equivalence between two `finite_dimensional`

vector spaces of the same `findim`

?

#### Johan Commelin (Jan 01 2021 at 16:03):

yes, I think Markus Himmel did that

#### Johan Commelin (Jan 01 2021 at 16:04):

I forgot the name of the result...

#### Heather Macbeth (Jan 01 2021 at 16:05):

I tried searching for `linear_equiv`

in `linear_algebra.finite_dimensional`

and couldn't see it.

#### Adam Topaz (Jan 01 2021 at 16:06):

This is true in general, not just for finite dimensional. Maybe that helps in finding it?

#### Johan Commelin (Jan 01 2021 at 16:06):

Is this what you want: `src/linear_algebra/invariant_basis_number.lean`

?

#### Johan Commelin (Jan 01 2021 at 16:07):

or is that in the wrong direction?

#### Adam Topaz (Jan 01 2021 at 16:08):

(Heather are you formalizing projective spaces? :smile: )

#### Heather Macbeth (Jan 01 2021 at 16:08):

I think it might be in the wrong direction, yes.

#### Heather Macbeth (Jan 01 2021 at 16:09):

Adam Topaz said:

(Heather are you formalizing projective spaces? :smile: )

No ...

https://github.com/leanprover-community/mathlib/tree/sphere

#### Adam Topaz (Jan 01 2021 at 16:10):

Oh nice! I figured it was projective spaces because of the span notation we were discussing a few day ago.

#### Adam Topaz (Jan 01 2021 at 16:12):

anyway, the closest I can find so far to the problem at hand is this docs#equiv_of_is_basis

#### Heather Macbeth (Jan 01 2021 at 16:14):

That looks good, thanks! I don't understand why it's not named `linear_equiv_of_is_basis`

, though :)

#### Adam Topaz (Jan 01 2021 at 16:14):

Yeah I agree.

#### Adam Topaz (Jan 01 2021 at 16:15):

docs#cardinal.eq gets you essentially all the way to what you want.

#### Adam Topaz (Jan 01 2021 at 16:16):

And this docs#is_basis.mk_eq_dim''

#### Adam Topaz (Jan 01 2021 at 16:27):

```
import linear_algebra
import linear_algebra.dimension
open_locale classical
universe u
variables (K : Type*) [field K] (V W : Type u)
[add_comm_group V] [add_comm_group W] [vector_space K V] [vector_space K W]
example (cond : vector_space.dim K V = vector_space.dim K W) : nonempty (V ≃ₗ[K] W) :=
begin
obtain ⟨B,hB⟩ := exists_is_basis K V,
obtain ⟨C,hC⟩ := exists_is_basis K W,
have h1 := is_basis.mk_eq_dim'' hB,
have h2 := is_basis.mk_eq_dim'' hC,
have h3 : cardinal.mk B = cardinal.mk C, by cc,
rw cardinal.eq at h3,
cases h3,
refine ⟨equiv_of_is_basis hB hC h3⟩,
end
```

#### Heather Macbeth (Jan 01 2021 at 16:28):

Wonderful! Can you PR it?

#### Adam Topaz (Jan 01 2021 at 16:29):

sure.

#### Adam Topaz (Jan 01 2021 at 16:29):

Which file should it go in?

#### Adam Topaz (Jan 01 2021 at 16:30):

Oh, there is one annoying thing -- to even state that the two vector spaces have the same dimension, they need to come from the same universe.

#### Heather Macbeth (Jan 01 2021 at 16:30):

I think `linear_algebra.dimension`

#### Heather Macbeth (Jan 01 2021 at 16:31):

Adam Topaz said:

Oh, there is one annoying thing -- to even state that the two vector spaces have the same dimension, they need to come from the same universe.

We just need a version for `finite_dimensional`

and `findim`

, that avoids all those issues.

#### Adam Topaz (Jan 01 2021 at 16:31):

You can still have finite dimensional vector spaces in different universes.

#### Adam Topaz (Jan 01 2021 at 16:32):

Oh I see what you mean.

#### Adam Topaz (Jan 01 2021 at 16:32):

The dimension would be in nat, not in cardinal

#### Adam Topaz (Jan 01 2021 at 16:48):

Okay, I pushed to this branch branch#lin_equiv_of_basis_equiv

#### Adam Topaz (Jan 01 2021 at 16:49):

Is there a `finite_dimensional`

analogue of docs#linear_equiv.dim_eq with `findim`

?

#### Heather Macbeth (Jan 01 2021 at 17:22):

Thanks!

Adam Topaz said:

Is there a

`finite_dimensional`

analogue of docs#linear_equiv.dim_eq with`findim`

?

#### Adam Topaz (Jan 01 2021 at 17:24):

I have the finite-dimensional case essentially done too (with no universe limitations). I'll open a PR soon.

#### Adam Topaz (Jan 01 2021 at 17:36):

#### Patrick Massot (Jan 01 2021 at 18:39):

I'm skeptical that you really want the conclusion of the lemma to be `nonempty (V ≃ₗ[K] V₂)`

. The first thing you'll do when using the lemma will be to extract an isomorphism. Why not making it a def?

#### Patrick Massot (Jan 01 2021 at 18:42):

I'm also surprised those lemmas are no already there somehow. I would wait for @Anne Baanen to comment on this.

#### Adam Topaz (Jan 01 2021 at 18:46):

I mostly used `nonempty`

to make it a `Prop`

, which is useful for the if and only if statement. I can make a `def`

to get the linear equiv as well, but I agree that we should wait for @Anne Baanen :)

#### Anne Baanen (Jan 02 2021 at 06:05):

Patrick Massot said:

I'm also surprised those lemmas are no already there somehow. I would wait for Anne Baanen to comment on this.

I don't recall seeing something like `linear_equiv.of_findim_eq`

, only the equivalences assuming a basis, so I think this is indeed a hole in the library.

#### Anne Baanen (Jan 02 2021 at 06:18):

Adam Topaz said:

I mostly used

`nonempty`

to make it a`Prop`

, which is useful for the if and only if statement. I can make a`def`

to get the linear equiv as well, but I agree that we should wait for Anne Baanen :)

The `nonempty`

situation as it is in the PR right now seems optimal to me: cardinal equality is expressed in `nonempty`

, so the first result also uses `nonempty`

and the next ones apply `classical.choice`

:+1:

Last updated: May 19 2021 at 02:10 UTC