English
If x is a transcendence basis over R in E, then the adjoin of range x over R is algebraic over E.
Русский
Если x является базисом трансцендентности над R в E, то адъюнкт диапазона x над R алгебраически над E.
LaTeX
$$$ Algebra.IsAlgebraic (adjoin R (range x)) E$$$
Lean4
theorem isAlgebraic_iff [IsDomain S] [NoZeroDivisors A] {ι : Type*} {v : ι → A} (hv : IsTranscendenceBasis R v) :
Algebra.IsAlgebraic S A ↔ ∀ i, IsAlgebraic S (v i) :=
by
refine ⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩
let Rv := adjoin R (range v)
let Sv := adjoin S (range v)
have : Algebra.IsAlgebraic S Sv := by simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
have le : Rv ≤ Sv.restrictScalars R := by rw [Subalgebra.restrictScalars_adjoin]; exact le_sup_right
letI : Algebra Rv Sv := (Subalgebra.inclusion le).toAlgebra
have : IsScalarTower Rv Sv A := .of_algebraMap_eq fun x ↦ rfl
have := (algebraMap R S).domain_nontrivial
have := hv.isAlgebraic
have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)
exact .trans _ Sv _
