English
If H: AlgebraicIndependent S (g ∘ x) and hf is injective and a certain compatibility holds, then AlgebraicIndependent R x.
Русский
Пусть H: алгебраически независимо над S элементами g∘x, условие инъективности hf и совместимость отображений, тогда x алгебраически независим над R.
LaTeX
$$$H: \\operatorname{AlgIndep}_S(g \\circ x) \\land \\text{Injective}(f) \\land \\bigl(\\cdot\\bigr) \\Rightarrow \\operatorname{AlgIndep}_R x$$$
Lean4
theorem of_ringHom_of_comp_eq (H : AlgebraicIndependent S (g ∘ x)) (hf : Function.Injective f)
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : AlgebraicIndependent R x :=
by
rw [algebraicIndependent_iff] at H ⊢
intro p hp
have :=
H (p.map f) <| by
have : (g : A →+* B) _ = _ := congr(g $hp)
rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
exact map_injective (f : R →+* S) hf (by rwa [map_zero])
