English
IsTranscendenceBasis R x is equivalent to Algebra.IsAlgebraic on the adjoin of range x in A if x is algebraically independent over R.
Русский
IsTranscendenceBasis R x эквивалентно алгебраическому над A адъюнкту диапазона x, если x алгебраически независим над R.
LaTeX
$$$ IsTranscendenceBasis R x \iff Algebra.IsAlgebraic (Subtype fun x_1 => x_1 \in \mathrm{adjoin} R (range x)) A$$
Lean4
theorem isTranscendenceBasis_iff_isAlgebraic [Nontrivial R] (ind : AlgebraicIndependent R x) :
IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (adjoin R (range x)) A :=
by
refine ⟨(·.isAlgebraic), fun alg ↦ ⟨ind, fun s ind_s hxs ↦ of_not_not fun hxs' ↦ ?_⟩⟩
have : ¬s ⊆ range x := (hxs' <| hxs.antisymm ·)
have ⟨a, has, hax⟩ := not_subset.mp this
rw [show range x = Subtype.val '' range (Set.inclusion hxs) by
rw [← range_comp, val_comp_inclusion, Subtype.range_val]] at alg
refine ind_s.transcendental_adjoin (s := range (inclusion hxs)) (i := ⟨a, has⟩) ?_ (alg.1 _)
simpa using hax
