Zulip Chat Archive

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 E1/KE_1/K and E2/KE_2/K, contained in some larger field LL, we have that E1E2/KE_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