Finite dimensional vector space over a finite field

Stream: Is there code for X?

[Patrick Lutz]

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?

[Johan Commelin]

I think so

[Johan Commelin]

vector_space.card_fintype?

[Patrick Lutz]

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?

[Patrick Lutz]

Oh wait, nevermind

[Patrick Lutz]

module.fintype_of_fintype takes care of it

[Patrick Lutz]

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?

[Aaron Anderson]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Aaron Anderson]

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

[Aaron Anderson]

Yeah, it looks like that’s standard.

[Aaron Anderson]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Markus Himmel]

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

[Patrick Lutz]

@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?

[Markus Himmel]

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

[Patrick Lutz]

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

[Markus Himmel]

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.

[Patrick Lutz]

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

[Patrick Lutz]

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

[Markus Himmel]

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

[Kevin Buzzard]

You're making type unification happen in a different order

[Markus Himmel]

Should it be obvious that the order matters?

[Patrick Lutz]

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.