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

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

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

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)

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?

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):

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!

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.

#5559

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

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: