Zulip Chat Archive

Stream: new members

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


Sebastian Monnet (Dec 20 2021 at 11:33):

Given a finite dimensional field extension E/KE/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 EE over KK. 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 (Dec 20 2021 at 11:34):

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 (Dec 20 2021 at 11:35):

finset.univ.image comp?

Sebastian Monnet (Dec 20 2021 at 11:47):

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 (Dec 20 2021 at 11:50):

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

Anne Baanen (Dec 20 2021 at 11:50):

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 (Dec 20 2021 at 11:52):

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 (Dec 20 2021 at 11:52):

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 (Dec 20 2021 at 11:53):

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 (Dec 20 2021 at 11:54):

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

Anne Baanen (Dec 20 2021 at 11:54):

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

Anne Baanen (Dec 20 2021 at 11:55):

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 (Dec 20 2021 at 11:55):

(Works on the community playground)

Anne Baanen (Dec 20 2021 at 11:56):

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 (Dec 20 2021 at 11:58):

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 (Dec 20 2021 at 12:01):

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 (Dec 20 2021 at 12:01):

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 (Dec 20 2021 at 12:23):

Anne Baanen said:

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

Should we add it?

Kevin Buzzard (Dec 20 2021 at 12:24):

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


Last updated: Dec 20 2023 at 11:08 UTC