English
There is a variant map' stating that if f is injective, then AlgebraicIndependent R (f ∘ x) holds, as a corollary of map.
Русский
Существует вариационный факт map', гласящий, что если f инъективен, то AlgebraicIndependent R (f ∘ x) сохраняется, как следствие map.
LaTeX
$$$\\\\mathrm{map'} \\\\text{ with injective } f \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R,(f\\\\circ x))$$$
Lean4
theorem map {f : A →ₐ[R] A'} (hf_inj : Set.InjOn f (adjoin R (range x))) : AlgebraicIndependent R (f ∘ x) :=
by
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
have h : ∀ p : MvPolynomial ι R, aeval x p ∈ (@aeval R _ _ _ _ _ ((↑) : range x → A)).range :=
by
intro p
rw [AlgHom.mem_range]
refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩
simp [Function.comp_def, aeval_rename]
intro x y hxy
rw [this] at hxy
rw [adjoin_eq_range] at hf_inj
exact hx (hf_inj (h x) (h y) hxy)
