Zulip Chat Archive

Stream: Is there code for X?

Topic: Finite dimensional vector space over a finite field


view this post on Zulip Patrick Lutz (Jul 29 2020 at 19:30):

I suspect this is not in mathlib, but I would love to be wrong: does mathlib already have some theorem to the effect that a finite dimensional vector space over a finite field is finite?

view this post on Zulip Johan Commelin (Jul 29 2020 at 19:30):

I think so

view this post on Zulip Johan Commelin (Jul 29 2020 at 19:31):

vector_space.card_fintype?

view this post on Zulip Patrick Lutz (Jul 29 2020 at 19:33):

It looks to me like to use that theorem you have to already know that the vector space V is fintype. Or am I missing something?

view this post on Zulip Patrick Lutz (Jul 29 2020 at 19:35):

Oh wait, nevermind

view this post on Zulip Patrick Lutz (Jul 29 2020 at 19:35):

module.fintype_of_fintype takes care of it

view this post on Zulip Patrick Lutz (Jul 29 2020 at 22:49):

The reason I wanted to know this was to show that a finite extension of a finite field is finite. I proved it like this

import linear_algebra.finite_dimensional

open finite_dimensional

noncomputable lemma finite_of_findim_over_finite (F : Type*) (E : Type*) [field F] [field E]
    [algebra F E] [fintype F] (hE : finite_dimensional F E) : fintype E :=
begin
    set s := classical.some (exists_is_basis_finite F E) with hs,
    have hs' := classical.some_spec (exists_is_basis_finite F E),
    rw  hs at hs',
    cases hs' with s_basis s_finite,
    have s_fintype : fintype s := set.finite.fintype s_finite,
    exact @module.fintype_of_fintype s F E (coe : s  E) _ _ _ s_fintype s_basis _,
end

but that feels a little gruesome. It feels like this should be something I can do in one line using module.fintype_of_fintype (and I believe it is, but I am just too inexperienced at Lean to see how). And does it really need to be uncomputable (I guess probably, since apparently module.fintype_of_fintype is)?

So, does anyone know how to make this proof totally trivial?

view this post on Zulip Aaron Anderson (Jul 30 2020 at 02:02):

This is what I did on the branch finite_fields_exist

variables {K : Type*} [field K] [fintype K]
variables {V : Type*} [add_comm_group V] [vector_space K V]

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
begin
  have b := classical.some_spec (finite_dimensional.exists_is_basis_finset K V),
  apply module.fintype_of_fintype b,
end

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:07):

@Aaron Anderson why did you make it a def rather than a lemma?

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:12):

Also, why does what you did work, but the following doesn't?

variables {K : Type*} [field K] [fintype K]
variables {V : Type*} [add_comm_group V] [vector_space K V]

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
begin
  apply module.fintype_of_fintype (classical.some_spec (finite_dimensional.exists_is_basis_finset K V)),
end

view this post on Zulip Aaron Anderson (Jul 30 2020 at 18:12):

Because fintype is data, not a prop. I might be totally wrong about that convention though, let me check the library.

view this post on Zulip Aaron Anderson (Jul 30 2020 at 18:14):

Yeah, it looks like that’s standard.

view this post on Zulip Aaron Anderson (Jul 30 2020 at 18:15):

I don’t recall what error I got shortening it... I bet it can be golfed somehow, maybe even term mode

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:17):

This is the error

type mismatch at application
  classical.some_spec (exists_is_basis_finset K V)
term
  exists_is_basis_finset K V
has type
   (b : finset V), is_basis K coe
but is expected to have type
   (x : module ?m_1 ?m_2), is_basis ?m_1 ?m_6

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:17):

It's not able to do some type inference I guess

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:17):

but what I don't understand is why it could do it in your proof but not in this one

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:18):

And I ran into somewhat similar problems which is why my proof above is more complicated than I wanted

view this post on Zulip Markus Himmel (Jul 30 2020 at 18:20):

The following works:

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
module.fintype_of_fintype (classical.some_spec (finite_dimensional.exists_is_basis_finset K V) : _)

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:21):

@Markus Himmel interesting. So in your proof you're explicitly giving lean a hint about how to do type inference? Or am I still confused?

view this post on Zulip Markus Himmel (Jul 30 2020 at 18:22):

I actually have no idea but it might be related to this?

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:23):

So (t : _) is used to tell Lean to not be too aggressive about premature type inference?

view this post on Zulip Markus Himmel (Jul 30 2020 at 18:24):

I think it somehow says to Lean "do not look at what this is being applied to". By doing the have line first in the tactic proof, you achieve a similar effect.

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:25):

I'm not sure I understand what you mean by "do not look at what this is being applied to"

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:25):

Shouldn't looking at what it's being applied to help Lean to make the correct type inference?

view this post on Zulip Markus Himmel (Jul 30 2020 at 18:25):

I don't think I understand either, to be honest.

view this post on Zulip Kevin Buzzard (Jul 30 2020 at 18:28):

You're making type unification happen in a different order

view this post on Zulip Markus Himmel (Jul 30 2020 at 18:30):

Should it be obvious that the order matters?

view this post on Zulip Patrick Lutz (Jul 30 2020 at 18:31):

Kevin Buzzard said:

You're making type unification happen in a different order

Sure, I understand this. But why does (t : _) give me the order I want? I guess the basic issue is that I don't know what the usual order is or how this syntax changes it.


Last updated: May 17 2021 at 15:13 UTC