English
Assuming a nontrivial base ring, x is a transcendence basis of A over R if and only if x is algebraically independent over R and the adjoin of its range is algebraic over A.
Русский
Пусть R не тривиально; x является базисом трансцендентности A над R тогда и только тогда, когда x алгебраически независимо над R и произведение (адъюнкт) адъюнкта диапазона x над A алгебраично над A.
LaTeX
$$$\ IsTranscendenceBasis R x \iff (AlgebraicIndependent R x \land Algebra.IsAlgebraic (adjoin R (range x)) A)$$$
Lean4
theorem isTranscendenceBasis_iff [Nontrivial R] (i : AlgebraicIndependent R x) :
IsTranscendenceBasis R x ↔
∀ (κ : Type w) (w : κ → A) (_ : AlgebraicIndependent R w) (j : ι → κ) (_ : w ∘ j = x), Surjective j :=
by
fconstructor
· rintro p κ w i' j rfl
have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)
rw [range_comp, ← @image_univ _ _ w] at p
exact range_eq_univ.mp (image_injective.mpr i'.injective p)
· intro p
use i
intro w i' h
specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
dsimp at q
rw [← image_univ, image_image] at q
simpa using q
