Zulip Chat Archive

Stream: new members

Topic: Finite field extension is fg

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

Given a finitely generated field extension E/KE/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 :=

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

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

"undergraduate mode"

Eric Rodriguez (Dec 22 2021 at 17:55):

I like the idea of open_locale undergraduate :)

Kevin Buzzard (Dec 23 2021 at 06:49):

Similarly vector_space should be an abbreviation for module in this locale

Last updated: Dec 20 2023 at 11:08 UTC