English
If for each i the polynomial f_i ∈ R[X] is transcendental over R, then the family {aeval(X_i)(f_i)} in MvPolynomial is algebraically independent over R.
Русский
Если для каждого i полином f_i ∈ R[X] трансцендентен над R, то семейство {aeval(X_i)(f_i)} в MvPolynomial(ι, R) алгебраически независимо над R.
LaTeX
$$$\\bigl(\\forall i, \\mathrm{Transcendental}_R(f_i)\\bigr) \\to \\mathrm{AlgebraicIndependent}_R\\bigl( i \\mapsto \\mathrm{Polynomial}.\\mathrm{aeval}(X_i : \\mathrm{MvPolynomial}_{ι}R) (f_i) \\bigr)$$$
Lean4
/-- If for each `i : ι`, `f_i : R[X]` is transcendental over `R`, then `{f_i(X_i) | i : ι}`
in `MvPolynomial ι R` is algebraically independent over `R`. -/
theorem algebraicIndependent_polynomial_aeval_X (f : ι → Polynomial R) (hf : ∀ i, Transcendental R (f i)) :
AlgebraicIndependent R fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i) :=
by
set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)
refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_
have hle : adjoin R (x '' t) ≤ supported R t :=
by
rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
intro _ h
rw [Set.mem_preimage]
refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle
