# 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/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 (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