## Stream: new members

### Topic: Compositum of finite field extension is finite

#### Sebastian Monnet (Dec 17 2021 at 16:13):

I need the fact that for finite field extensions $E_1/K$ and $E_2/K$, contained in some larger field $L$, we have that $E_1E_2 / K$ is also finite. Here is a statement of the lemma in Lean:

import tactic
import field_theory.galois
import data.set.basic
import algebra.group.basic

lemma comp_finrank_is_finrank (K L: Type*) [field K] [field L] [algebra K L] (E1 E2 : intermediate_field K L) : finite_dimensional K E1 ∧ finite_dimensional K E2 → finite_dimensional K ↥(Inf {E : intermediate_field K L | E = E1 ∨ E = E2}) :=
begin
sorry,
end


Does anyone know if this lemma already exists in mathlib? I've looked through a few of the field theory entries and I can't find anything that looks like this.

#### Anne Baanen (Dec 17 2021 at 16:16):

Maybe we have the statement for submodules? Edit: yes, docs#submodule.finite_dimensional_inf_left or docs#submodule.finite_dimensional_of_le

#### Kevin Buzzard (Dec 17 2021 at 16:21):

This is the wrong way -- here we want finite-dimensionality of the sup of two finite-dimensional things. Also note that submodules will not be enough -- the K-submodule generated by E1 and E2 might not be closed under multiplication.

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

We must have all of this somewhere though, it's surely used in Galois theory all over the place.

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

Oh yeah you're right - that was a typo

#### Kevin Buzzard (Dec 17 2021 at 16:23):

oh lol I didn't look at the code, I just read the LaTeX above it :-) I knew this would come up having thought a bit yesterday about what I know you're doing.

#### Sebastian Monnet (Dec 17 2021 at 16:24):

Kevin Buzzard said:

We must have all of this somewhere though, it's surely used in Galois theory all over the place.

I think it possibly isn't as common as you'd think. I remember only being introduced to the compositum of fields as the "unseen" part of a Galois theory exam. So you can clearly get to most of the main results without defining the compositum

#### Sebastian Monnet (Dec 17 2021 at 16:25):

So it's plausible that they never felt the need to state this while developing the Galois theory that's in Lean

#### Kevin Buzzard (Dec 17 2021 at 16:25):

yeah but in Lean we tend to do all this abstract stuff like subalgebras of an algebra are a lattice, and subalgebras with some finiteness property are a sublattice etc

#### Sebastian Monnet (Dec 17 2021 at 16:30):

Ah well, I guess I'll just bite the bullet and prove it myself

#### Kevin Buzzard (Dec 17 2021 at 16:30):

You could ask in #Is there code for X? ? Your question will get more visibility there.

#### Kevin Buzzard (Dec 17 2021 at 16:32):

It looks like it's missing though, it should probably be called subalgebra.finite_dimensional_sup to match docs#submodule.finite_dimensional_sup . It might be pretty gnarly to prove if you don't know the tricks; it looks painful to prove from first principles.

#### Sebastian Monnet (Dec 17 2021 at 16:33):

Kevin Buzzard said:

You could ask in #Is there code for X? ? Your question will get more visibility there.

Okay have done

#### Sebastian Monnet (Dec 17 2021 at 16:34):

I think we do have that adjoining an algebraic element gives a finite dimensional extension. We must have the tower law. So then using those two things it's some kind of induction by adjoining each basis element one at a time

#### Sebastian Monnet (Dec 17 2021 at 16:34):

I guess that probably is quite a big job... do you think I should just sorry it for now?

#### Kevin Buzzard (Dec 17 2021 at 16:35):

The idea is that you ask in #Is there code for X? and someone else does it for you.

#### Kevin Buzzard (Dec 17 2021 at 16:44):

All these come up all the time when you're developing the theory of normality of extensions, and normal closures etc. Let's see if the Galois theory kids (in Berkeley so probably currently asleep) have anything to add.

#### Anne Baanen (Dec 17 2021 at 17:27):

Kevin Buzzard said:

This is the wrong way -- here we want finite-dimensionality of the sup of two finite-dimensional things. Also note that submodules will not be enough -- the K-submodule generated by E1 and E2 might not be closed under multiplication.

Oops yes, sorry for the confusion.

Last updated: Dec 20 2023 at 11:08 UTC