English
If f and g are compatible ring homomorphisms via a commutative diagram, and a ∈ A is algebraic over R, then g(a) is algebraic over S, assuming appropriate injectivity and surjectivity conditions on f and g.
Русский
Если диаграмма по кольцам сопряжена через f и g и a алгебраичен над R, то g(a) алгебраичен над S, при условии инъективности f и сюръективности g и совместимости диаграммы.
LaTeX
$$$\forall f: FRS, \; \forall g: FAB, \; \forall a: A, \ IsAlgebraic(R, a) \Rightarrow IsAlgebraic(S, g(a))$ при соответствующих условиях совместимости.$$
Lean4
theorem ringHom_of_comp_eq (halg : IsAlgebraic R a) (hf : Function.Injective f)
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : IsAlgebraic S (g a) :=
by
obtain ⟨p, h1, h2⟩ := halg
refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
change aeval ((g : A →+* B) a) _ = 0
rw [← map_aeval_eq_aeval_map h, h2, map_zero]
