Zulip Chat Archive

Stream: Is there code for X?

Topic: Classification of finite-dimensional vector spaces


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 01 2021 at 16:03):

yes, I think Markus Himmel did that

view this post on Zulip Johan Commelin (Jan 01 2021 at 16:04):

I forgot the name of the result...

view this post on Zulip Heather Macbeth (Jan 01 2021 at 16:05):

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

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:06):

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

view this post on Zulip Johan Commelin (Jan 01 2021 at 16:06):

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

view this post on Zulip Johan Commelin (Jan 01 2021 at 16:07):

or is that in the wrong direction?

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:08):

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

view this post on Zulip Heather Macbeth (Jan 01 2021 at 16:08):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:14):

Yeah I agree.

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:15):

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

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:16):

And this docs#is_basis.mk_eq_dim''

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Jan 01 2021 at 16:28):

Wonderful! Can you PR it?

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:29):

sure.

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:29):

Which file should it go in?

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Jan 01 2021 at 16:30):

I think linear_algebra.dimension

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:31):

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

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:32):

Oh I see what you mean.

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:32):

The dimension would be in nat, not in cardinal

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:48):

Okay, I pushed to this branch branch#lin_equiv_of_basis_equiv

view this post on Zulip Adam Topaz (Jan 01 2021 at 16:49):

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

view this post on Zulip 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?

docs#linear_equiv.findim_eq?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 01 2021 at 17:36):

#5559

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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