English
For a family x: ι → A and a set s ⊆ ι, the family x restricted to s is algebraically independent over R iff there are no nontrivial polynomial relations p ∈ MvPolynomial s R with aeval x(p) = 0.
Русский
Для семейства x: ι → A и множества s ⊆ ι, независимость x по отношению к s над R эквивалентна тому, что не существует ненулевой полиномиальной зависимости p ∈ MvPolynomial s R с aeval x(p) = 0.
LaTeX
$$$\AlgebraicIndependent\_R\bigl(x \circ i\bigr) \iff \forall p \in \mathrm{MvPolynomial}(s,R),\ aeval\, x\ p = 0 \Rightarrow p = 0$$$
Lean4
theorem algebraicIndependent_comp_subtype {s : Set ι} :
AlgebraicIndependent R (x ∘ (↑) : s → A) ↔ ∀ p ∈ MvPolynomial.supported R s, aeval x p = 0 → p = 0 :=
by
have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp
have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
(injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
(rename_injective _ Subtype.val_injective)
simp [algebraicIndependent_iff, supported_eq_range_rename, *]
