Compositum of finite field extension is finite

Stream: new members

[Sebastian Monnet]

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]

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

[Kevin Buzzard]

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]

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

[Sebastian Monnet]

Oh yeah you're right - that was a typo

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Kevin Buzzard said:

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

Okay have done

[Sebastian Monnet]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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.