Compositum of finite field extensions is finite

Stream: Is there code for X?

[Sebastian Monnet]

(This question is copy-pasted from one in New Members)

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 ↥(Sup {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.

[Kevin Buzzard]

Your LaTeX is a sup but your code is an inf.(fixed)

[Kevin Buzzard]

I think the idiomatic way to ask the LaTeX question is

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

lemma subalgebra.finite_dimensional_sup (K L: Type*) [field K] [field L] [algebra K L]
  (E1 E2 : intermediate_field K L) (h1 : finite_dimensional K E1) (h2 : finite_dimensional K E2) :
  finite_dimensional K ↥(E1 ⊔ E2) :=
begin
  sorry,
end

and I agree that we don't seem to have it. Note that it won't follow from the corresponding statement about submodules docs#submodule.finite_dimensional_sup because the submodule sup is in general smaller than the subalgebra sup.

[Sebastian Monnet]

Kevin Buzzard said:

Your LaTeX is a sup but your code is an inf.

Fixed

[Yury G. Kudryashov]

AFAIR, we have transitivity, so you need to prove that the dimension of E1 ⊔ E2 over E1 is less than or equal to the dimension of E2 over K.

[Yury G. Kudryashov]

But I never used this part of the library.

[Adam Topaz]

Do we know that $E_1 \otimes E_2$ surjects onto it?

[Kevin Buzzard]

Oh I guess it should be called intermediate_field.finite_dimensional_sup

[Kevin Buzzard]

@Thomas Browning did you need this stuff for e.g. normal closure?

[Thomas Browning]

I can't remember seeing/using this sort of thing. We were just working with towers, I think.

[Kevin Buzzard]

It's a shame that this isn't there, this is the sort of thing which is quite fiddly if you're not an expert, and Sebastian is just starting.

[Kevin Buzzard]

I guess the lemma to prove is that if X spans E2 as a K-module then it spans E1 cup E2 as an E1-module

[Kevin Buzzard]

But stating that is fiddly

[Thomas Browning]

Here's a proof. I can start PRing it tomorrow, if you would like.

lemma alg_hom.range_comp {R A B C : Type*} [comm_semiring R] [semiring A] [semiring B]
[semiring C]
[algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).range = f.range.map g :=
set_like.coe_injective (set.range_comp g f)

lemma alg_hom.range_comp_le_range {R A B C : Type*} [comm_semiring R] [semiring A] [semiring B]
[semiring C]
[algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).range ≤ g.range :=
set_like.coe_mono (set.range_comp_subset_range f g)

lemma subalgebra.mem_sup_left {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
{S T : subalgebra R A} : ∀ {x : A}, x ∈ S → x ∈ S ⊔ T :=
show S ≤ S ⊔ T, from le_sup_left

lemma subalgebra.mem_sup_right {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
{S T : subalgebra R A} : ∀ {x : A}, x ∈ T → x ∈ S ⊔ T :=
show T ≤ S ⊔ T, from le_sup_right

lemma subalgebra.mul_mem_sup {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
{S T : subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
(S ⊔ T).mul_mem (subalgebra.mem_sup_left hx) (subalgebra.mem_sup_right hy)

lemma algebra.tensor_product.product_map_range {R A B S : Type*} [comm_semiring R]
[semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S]
(f : A →ₐ[R] S) (g : B →ₐ[R] S) :
(algebra.tensor_product.product_map f g).range = f.range ⊔ g.range :=
begin
refine le_antisymm _ (sup_le _ _),
{ have := tensor_product.span_tmul_eq_top R A B,
replace : algebra.adjoin R {t : A ⊗ B | ∃ (a : A) (b : B), a ⊗ₜ[R] b = t} = ⊤ :=
top_le_iff.mp ((eq_top_iff.mp this).trans (algebra.span_le_adjoin R _)),
rw [←algebra.map_top, ←this, ←algebra.adjoin_image, algebra.adjoin_le_iff],
rintros _ ⟨_, ⟨a, b, rfl⟩, rfl⟩,
rw algebra.tensor_product.product_map_apply_tmul,
exact subalgebra.mul_mem_sup (f.mem_range_self a) (g.mem_range_self b) },
{ conv_lhs { rw ← algebra.tensor_product.product_map_left f g },
apply alg_hom.range_comp_le_range },
{ conv_lhs { rw ← algebra.tensor_product.product_map_right f g },
apply alg_hom.range_comp_le_range },
end

lemma subalgebra.finite_dimensional_sup {K L : Type*} [field K] [comm_ring L] [algebra K L]
(E1 E2 : subalgebra K L) [finite_dimensional K E1] [finite_dimensional K E2] :
finite_dimensional K ↥(E1 ⊔ E2) :=
begin
let g := algebra.tensor_product.product_map E1.val E2.val,
suffices : g.to_linear_map.range = (E1 ⊔ E2).to_submodule,
{ have key := g.to_linear_map.finite_dimensional_range,
rwa this at key },
suffices : g.range = E1 ⊔ E2,
{ rw ← this,
refl },
rw [algebra.tensor_product.product_map_range, E1.range_val, E2.range_val],
end

lemma intermediate_field.range_val {K L : Type*} [field K] [field L] [algebra K L]
(S : intermediate_field K L) : S.val.range = S.to_subalgebra :=
S.to_subalgebra.range_val

lemma le_integral_closure_iff_is_integral {R A : Type*} [comm_ring R] [comm_ring A]
[algebra R A] {S : subalgebra R A} : S ≤ integral_closure R A ↔ algebra.is_integral R S :=
begin
have : (∀ x : S, is_integral R (algebra_map S A x)) ↔ (∀ x : S, is_integral R x) :=
forall_congr (λ x, is_integral_algebra_map_iff subtype.coe_injective),
exact set_like.forall.symm.trans this,
end

lemma is_field_of_is_integral_of_is_field'
{R S : Type*} [field R] [comm_ring S] [is_domain S]
[algebra R S] (H : algebra.is_integral R S) (hRS : function.injective (algebra_map R S)) :
is_field S :=
begin
refine ⟨⟨0, 1, zero_ne_one⟩, mul_comm, λ x hx, _⟩,
have key0 := fg_adjoin_singleton_of_integral x (H x),
let A := algebra.adjoin R ({x} : set S),
let f : A →ₗ[R] A :=
{ to_fun := λ y, ⟨x, algebra.mem_adjoin_iff.mpr (subring.mem_closure.mpr (λ T hT,
show _, from set.singleton_subset_iff.mp (set.union_subset_iff.mp hT).2))⟩ * y,
map_add' := λ y z, mul_add _ y z,
map_smul' := λ y z, mul_smul_comm y _ z, },
have key : function.injective f,
{ rw [←linear_map.ker_eq_bot, eq_bot_iff],
intros y hy,
exact (eq_zero_or_eq_zero_of_mul_eq_zero hy).resolve_left (λ h, hx (subtype.ext_iff.mp h)) },
haveI key' : is_noetherian R A.to_submodule := is_noetherian_of_fg_of_noetherian A.to_submodule
(fg_adjoin_singleton_of_integral x (H x)),
haveI this : module.finite R A.to_submodule := module.is_noetherian.finite R A,
tactic.unfreeze_local_instances,
change module.finite R A at this,
obtain ⟨y, hy⟩ := @linear_map.surjective_of_injective R A _ _ _ _ f key 1,
exact ⟨y, subtype.ext_iff.mp hy⟩,
end

lemma intermediate_field.sup_to_subalgebra {K L : Type*} [field K] [field L] [algebra K L]
(E1 E2 : intermediate_field K L) [finite_dimensional K E1] [finite_dimensional K E2] :
(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra :=
begin
have h1 : algebra.is_integral K E1 :=
(is_algebraic_iff_is_integral' K).mp algebra.is_algebraic_of_finite,
have h2 : algebra.is_integral K E2 :=
(is_algebraic_iff_is_integral' K).mp algebra.is_algebraic_of_finite,
have h3 : algebra.is_integral K ↥(E1.to_subalgebra ⊔ E2.to_subalgebra) :=
le_integral_closure_iff_is_integral.mp (sup_le
(le_integral_closure_iff_is_integral.mpr h1) (le_integral_closure_iff_is_integral.mpr h2)),
have h4 := is_field_of_is_integral_of_is_field' h3 (ring_hom.injective _),
let S : intermediate_field K L := (E1.to_subalgebra ⊔ E2.to_subalgebra).to_intermediate_field
(λ x hx, by
{ by_cases hx' : x = 0,
{ rw [hx', inv_zero],
exact (E1.to_subalgebra ⊔ E2.to_subalgebra).zero_mem },
{ obtain ⟨y, hy⟩ := h4.mul_inv_cancel
(show (⟨x, hx⟩ : E1.to_subalgebra ⊔ E2.to_subalgebra) ≠ 0,
from (λ h, hx' (subtype.ext_iff.mp h))),
have key : ↑y = x⁻¹ := eq_inv_of_mul_right_eq_one (subtype.ext_iff.mp hy),
rw ← key,
exact y.2 } }),
exact le_antisymm (show E1 ⊔ E2 ≤ S, from sup_le
(show E1.to_subalgebra ≤ E1.to_subalgebra ⊔ E2.to_subalgebra, from le_sup_left)
(show E2.to_subalgebra ≤ E1.to_subalgebra ⊔ E2.to_subalgebra, from le_sup_right))
(sup_le (show E1 ≤ E1 ⊔ E2, from le_sup_left)
(show E2 ≤ E1 ⊔ E2, from le_sup_right)),
end

lemma intermediate_field.finite_dimensional_sup {K L : Type*} [field K] [field L] [algebra K L]
(E1 E2 : intermediate_field K L) [h1 : finite_dimensional K E1] [h2 : finite_dimensional K E2] :
finite_dimensional K ↥(E1 ⊔ E2) :=
begin
let g := algebra.tensor_product.product_map E1.val E2.val,
suffices : g.to_linear_map.range = (E1 ⊔ E2).to_subalgebra.to_submodule,
{ have key := g.to_linear_map.finite_dimensional_range,
rwa this at key },
suffices : g.range = (E1 ⊔ E2).to_subalgebra,
{ rw ← this,
refl },
rw [algebra.tensor_product.product_map_range, E1.range_val, E2.range_val],
exact (intermediate_field.sup_to_subalgebra E1 E2).symm,
end

[Kevin Buzzard]

Oh my goodness! Thank you so much Thomas!

[Sebastian Monnet]

Thanks Thomas, that’s incredibly helpful!

[Kevin Buzzard]

So I can't quite get Thomas' code running because I seem to be missing an instance.

instance foo (K L M : Type*) [field K] [comm_ring L] [comm_ring M] [algebra K L] [algebra K M]
  [finite_dimensional K L] [finite_dimensional K M] : finite_dimensional K (L ⊗[K] M) :=
sorry

Am I missing an import?

[Thomas Browning]

You're probably missing linear_algebra/tensor_product_basis.lean. Sorry, I should have added imports.

[Thomas Browning]

Here's the PR: #10938

[Kevin Buzzard]

Thanks Thomas!

I think that to do the stuff with normality we need a little more about splitting fields, for example "if L/K is an extension, and f in K[X] splits in E_i for a bunch of subfields, then it splits in their Inf".

[Thomas Browning]

That particular thing doesn't sound too hard, since you can look at the roots of f. One way of doing this is to factor f in L (in terms of a multiset of elements of L), show that each root lies in the Inf, then construct a multiset in the Inf, and finally invoke the lemma about splitting iff there exists a multiset.

[Thomas Browning]

Is there a specific goal that all this is building up to?

[Kevin Buzzard]

Topology on $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}).$

[Kevin Buzzard]

We already have it, but we're trying to do it properly (i.e. make a better definition for which it will be possible to develop an API)