## Stream: new members

### Topic: Finite field extension is fg

#### Sebastian Monnet (Dec 22 2021 at 16:47):

Given a finitely generated field extension $E/K$, I would like to prove that \top : subalgebra K E is fg over K. For context, I am trying to prove prod_min_polys_monic in the following code.

import tactic
import field_theory.galois
import data.set.basic
import algebra.group.basic
import ring_theory.tensor_product
import topology.algebra.filter_basis
import order.filter.bases
import linear_algebra.finite_dimensional
import data.finset.basic
import data.set.finite
import data.polynomial.eval

open_locale classical

noncomputable def root_finset {K : Type*} [field K] (p : polynomial K) (L : Type*) [field L] [algebra K L] : finset L :=
(p.map (algebra_map K L)).roots.to_finset

lemma root_eval_zero {K : Type*} [field K] {p : polynomial K} {L : Type*} [field L] [algebra K L] {x : L} (hx : x ∈ root_finset p L) :
polynomial.eval₂ (algebra_map K L) x p = 0 :=
begin
sorry,
end

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

noncomputable def prod_min_polys {K E : Type*} [field K] [field E] [algebra K E]
(h_findim : finite_dimensional K E) : polynomial K :=
finset.prod (min_polys h_findim) id

lemma prod_min_polys_monic {K E : Type*} [field K] [field E] [algebra K E]
(h_findim : finite_dimensional K E) :
(prod_min_polys h_findim).monic :=
begin
refine polynomial.monic_prod_of_monic (min_polys h_findim) id _,
intros p hp,
unfold min_polys at hp,
rw finset.mem_image at hp,
cases hp with i hp,
cases hp with hi hp,
rw ← hp,
apply minpoly.monic,
let v : E := (finite_dimensional.fin_basis K E) i,
change is_integral K v,
refine is_integral_of_mem_of_fg (⊤ : subalgebra K E) _ (v : E) _,
{
sorry,
},
{
simp,
},
end


I've looked through mathlib but I can't find any results linking finite_dimensional K E with \top.fg. Can anyone help?

#### Eric Rodriguez (Dec 22 2021 at 16:50):

I think you'll need docs#is_noetherian.iff_fg (I think this was the name)

#### Eric Wieser (Dec 22 2021 at 16:51):

It's basically true by definition I think? docs#module.finite is defined as (⊤ : submodule R A).fg, and there's a lemma docs#subalgebra.fg_of_submodule_fg that says if the top submodule is fg so is the top subalgebra

#### Eric Rodriguez (Dec 22 2021 at 16:51):

finite_dimensional is defeq to module.finite

#### Eric Wieser (Dec 22 2021 at 16:53):

So I think the answer is subalgebra.fg_of_submodule_fg module.finite.out

#### Sebastian Monnet (Dec 22 2021 at 16:59):

Thank you! The solution was exact h_findim.out.

#### Kevin Buzzard (Dec 22 2021 at 17:03):

Nice :-) The joys of definitional equality!

#### Riccardo Brasca (Dec 22 2021 at 17:28):

If someone is ready to erase finite_dimensional from mathlib you are welcome :)

#### Kevin Buzzard (Dec 22 2021 at 17:33):

It should be an abbreviation defined in a locale

#### Kevin Buzzard (Dec 22 2021 at 17:33):

I like the idea of open_locale undergraduate :)
Similarly vector_space should be an abbreviation for module in this locale