English
If H: AlgebraicIndependent R x and f is surjective, g injective, and a compatibility holds, then AlgebraicIndependent S (g ∘ x).
Русский
Если H: алгебраически независимо над R x, f сюрьективен, g инъективен и выполняется совместимость отображений, тогда AlgebraicIndependent S (g ∘ x).
LaTeX
$$$H: \\operatorname{AlgIndep}_R x \\land \\text{Surjective}(f) \\land \\text{Injective}(g) \\land h: \\cdot \\Rightarrow \\operatorname{AlgIndep}_S(g \\circ x)$$$
Lean4
theorem ringHom_of_comp_eq (H : AlgebraicIndependent R x) (hf : Function.Surjective f) (hg : Function.Injective g)
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : AlgebraicIndependent S (g ∘ x) :=
by
rw [algebraicIndependent_iff] at H ⊢
intro p hp
obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
rw [H q (hg (by rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom])),
map_zero]
