Constructing a term of `finset` from function from `fin (n)`

Stream: new members

[Sebastian Monnet]

Given a finite dimensional field extension $E/K$, I would like to construct a term of finset(polynomial K)containing the minimum polynomials of a generating set. The idea is that I would then like to take the splitting field of their product to construct a normal closure of $E$ over $K$. Here is my attempt so far:

import field_theory.galois

def min_polys {K E : Type*} [field K] [field E] [algebra K E] (h_findim : finite_dimensional K E) : finset (polynomial K) :=
begin
  let B := coe_fn(finite_dimensional.fin_basis K E),
  let minpoly_func : E → polynomial(K) := λ x, minpoly K x,
  let comp := minpoly_func ∘ B,
  sorry,
end

So I have a function comp : fin(finkrank K E) \to poly K, and I would like to view its image as a finset, so that I can take the product of its elements. Does anyone have any suggestions for how to do this?

[Anne Baanen]

I know we have docs#finset.image for the image of a finset, I don't think there's something specifically for the range of a function.

[Yaël Dillies]

finset.univ.image comp?

[Sebastian Monnet]

Yaël Dillies said:

finset.univ.image comp?

I tried

def min_polys {K E : Type*} [field K] [field E] [algebra K E] (h_findim : finite_dimensional K E) : finset (polynomial K) :=
begin
  let B := coe_fn(finite_dimensional.fin_basis K E),
  let minpoly_func : E → polynomial(K) := λ x, minpoly K x,
  let comp := minpoly_func ∘ B,
  let thing := finset.univ.image comp,
end

and I got a type class inference error. I guess it's because Lean doesn't know that fin (finite_dimensional.finrank K E) is a finset?

[Yaël Dillies]

Try #check fin.fintype. Maybe you're missing the import of data.fintype.basic.

[Anne Baanen]

I get the following error:

failed to synthesize type class instance for
K : Type ?,
E : Type ?,
_inst_1 : field K,
_inst_2 : field E,
_inst_3 : algebra K E,
h_findim : finite_dimensional K E,
B : fin (finite_dimensional.finrank K E) → E := ⇑(finite_dimensional.fin_basis K E),
minpoly_func : E → polynomial K := λ (x : E), minpoly K x,
comp : fin (finite_dimensional.finrank K E) → polynomial K := minpoly_func ∘ B
⊢ decidable_eq (polynomial K)

[Sebastian Monnet]

Anne Baanen said:

I get the following error:

failed to synthesize type class instance for
K : Type ?,
E : Type ?,
_inst_1 : field K,
_inst_2 : field E,
_inst_3 : algebra K E,
h_findim : finite_dimensional K E,
B : fin (finite_dimensional.finrank K E) → E := ⇑(finite_dimensional.fin_basis K E),
minpoly_func : E → polynomial K := λ (x : E), minpoly K x,
comp : fin (finite_dimensional.finrank K E) → polynomial K := minpoly_func ∘ B
⊢ decidable_eq (polynomial K)

Yeah this is the same error I get

[Sebastian Monnet]

Yaël Dillies said:

Try #check fin.fintype. Maybe you're missing the import of data.fintype.basic.

Gives me fin (finite_dimensional.finrank K E)

[Anne Baanen]

The important line is the last one: the instance decidable_eq (polynomial K) was not found, which is needed to allow Lean to compute exactly which polynomials should be in the set. You can fix it in one of two ways: the easy way is to add a line open_locale classical after the imports that says we're not interested in computing, or add a [decidable_eq K] parameter to your definition that pushes this requirement to the user of your definition.

[Anne Baanen]

Wait hang on, docs#polynomial.decidable_eq doesn't exist?

[Anne Baanen]

So I guess the second solution doesn't apply, and open_locale classical it is:

[Anne Baanen]

import field_theory.adjoin

open_locale classical

def min_polys {K E : Type*} [field K] [field E] [algebra K E] (h_findim : finite_dimensional K E) : finset (polynomial K) :=
begin
  let B := coe_fn(finite_dimensional.fin_basis K E),
  let minpoly_func : E → polynomial(K) := λ x, minpoly K x,
  let comp := minpoly_func ∘ B,
  let thing := finset.univ.image comp,
end

[Anne Baanen]

(Works on the community playground)

[Anne Baanen]

Completed definition:

import field_theory.adjoin

open_locale classical

noncomputable def min_polys {K E : Type*} [field K] [field E] [algebra K E] (h_findim : finite_dimensional K E) : finset (polynomial K) :=
finset.univ.image (minpoly K ∘ finite_dimensional.fin_basis K E)

[Anne Baanen]

Note that I added noncomputable in front of def, which is required because we don't have an algorithm to determine the list of polynomials. You can also put noncomputable theory after the open_locale line, then Lean will automatically figure out where to put noncomputable.

[Sebastian Monnet]

Nice, thank you @Anne Baanen. As an aside, is it a normal workflow for definitions to start off in tactic mode and then tidy things up to term mode? Obviously it's valid, but is it what most people do?

[Anne Baanen]

Yes, I do that regularly. Generally you want definitions to be in term mode, so you know exactly what unfold min_polys will give you.

[Yaël Dillies]

Anne Baanen said:

Wait hang on, docs#polynomial.decidable_eq doesn't exist?

Should we add it?

[Kevin Buzzard]

For proofs if I realise at the end that it's easy to rewrite in term mode, I often do, simply because it makes them compile a bit quicker. For definitions I try to stay in term mode at all times (unless I'm filling in a subproof) because I'm terrified about what random junk a tactic will add to my term