English
If L is an intermediate field of K/F and either F/E or F/L is algebraic, then the adjoin of E with L over L yields the same subalgebra as the algebraic adjoin: (adjoin E (L:Set K)).toSubalgebra = Algebra.adjoin E (L:Set K).
Русский
Если L — промежуточное поле K/F и либо F/E, либо F/L алгебраические, то при присоединении E к L получаем ту же подалгебру, что и алгебраическое присоединение.
LaTeX
$$$(\text{adjoin } E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) \quad\text{при } Algebra.IsAlgebraic F E \lor Algebra.IsAlgebraic F L$$
Lean4
/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `E(L) = E[L]`. -/
theorem adjoin_toSubalgebra_of_isAlgebraic (L : IntermediateField F K)
(halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
(adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
by
let i := IsScalarTower.toAlgHom F E K
let E' := i.fieldRange
let i' : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField i
have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
apply_fun _ using Subalgebra.restrictScalars_injective F
rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin]
dsimp only [← E'.coe_type_toSubalgebra]
rw [Algebra.restrictScalars_adjoin F E'.toSubalgebra]
exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)
