English
In a field tower F ⊆ E ⊆ K with L ⊆ K finite over F, if either E/F or L/F is algebraic, then [E(L):E] ≤ [L:F]. Equivalently, rank_E(adjoin_E(L)) ≤ rank_F(L).
Русский
В тензорной башне полей F ⊆ E ⊆ K, если L ⊆ K, и либо E/F, либо L/F алгебраичны, то отношение размерностей удовлетворяет [E(L):E] ≤ [L:F].
LaTeX
$$$\operatorname{rank}_E\big(\operatorname{adjoin}_E(L)\big) \le \operatorname{rank}_F(L)$ under algebraicity hypotheses$$
Lean4
/-- A compositum of splitting fields is a splitting field -/
theorem isSplittingField_iSup {p : ι → K[X]} {s : Finset ι} (h0 : ∏ i ∈ s, p i ≠ 0)
(h : ∀ i ∈ s, (p i).IsSplittingField K (t i)) :
(∏ i ∈ s, p i).IsSplittingField K (⨆ i ∈ s, t i : IntermediateField K L) :=
by
let F : IntermediateField K L := ⨆ i ∈ s, t i
have hF : ∀ i ∈ s, t i ≤ F := fun i hi ↦ le_iSup_of_le i (le_iSup (fun _ ↦ t i) hi)
simp only [isSplittingField_iff] at h ⊢
refine
⟨splits_prod (algebraMap K F) fun i hi ↦
splits_comp_of_splits (algebraMap K (t i)) (inclusion (hF i hi)).toRingHom (h i hi).1,
?_⟩
simp only [rootSet_prod p s h0, ← Set.iSup_eq_iUnion, (@gc K _ L _ _).l_iSup₂]
exact iSup_congr fun i ↦ iSup_congr fun hi ↦ (h i hi).2
