Classification of finite-dimensional vector spaces

Stream: Is there code for X?

[Heather Macbeth]

Do we have, there exists a linear equivalence between two finite_dimensional vector spaces of the same findim?

[Johan Commelin]

yes, I think Markus Himmel did that

[Johan Commelin]

I forgot the name of the result...

[Heather Macbeth]

I tried searching for linear_equiv in linear_algebra.finite_dimensional and couldn't see it.

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

or is that in the wrong direction?

[Adam Topaz]

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

[Heather Macbeth]

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

[Heather Macbeth]

Adam Topaz said:

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

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

[Adam Topaz]

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

[Adam Topaz]

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

[Heather Macbeth]

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

[Adam Topaz]

Yeah I agree.

[Adam Topaz]

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

[Adam Topaz]

And this docs#is_basis.mk_eq_dim''

[Adam Topaz]

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]

Wonderful! Can you PR it?

[Adam Topaz]

sure.

[Adam Topaz]

Which file should it go in?

[Adam Topaz]

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]

I think linear_algebra.dimension

[Heather Macbeth]

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]

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

[Adam Topaz]

Oh I see what you mean.

[Adam Topaz]

The dimension would be in nat, not in cardinal

[Adam Topaz]

Okay, I pushed to this branch branch#lin_equiv_of_basis_equiv

[Adam Topaz]

Is there a finite_dimensional analogue of docs#linear_equiv.dim_eq with findim?

[Heather Macbeth]

Thanks!
Adam Topaz said:

Is there a finite_dimensional analogue of docs#linear_equiv.dim_eq with findim?

docs#linear_equiv.findim_eq?

[Adam Topaz]

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

[Adam Topaz]

#5559

[Patrick Massot]

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]

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

[Adam Topaz]

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]

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]

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: