Finite field extension is fg

Stream: new members

[Sebastian Monnet]

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


-- Adjoin roots
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]

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

[Eric Wieser]

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]

finite_dimensional is defeq to module.finite

[Eric Wieser]

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

[Sebastian Monnet]

Thank you! The solution was exact h_findim.out.

[Kevin Buzzard]

Nice :-) The joys of definitional equality!

[Riccardo Brasca]

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

[Kevin Buzzard]

It should be an abbreviation defined in a locale

[Kevin Buzzard]

"undergraduate mode"

[Eric Rodriguez]

I like the idea of open_locale undergraduate :)

[Kevin Buzzard]

Similarly vector_space should be an abbreviation for module in this locale