English
If a is algebraic over R after mapping through a chain of rings, then the corresponding image is algebraic over the target ring via the composition equality.
Русский
Если образ a после композиции кольцевых отображений алгебраичен над R, то образ в целевом кольце алгебраичен над соответствующим кольцом.
LaTeX
$$$[Algebra.IsAlgebraic S B] \Rightarrow IsAlgebraic R a$ по равенству композиции.$$
Lean4
theorem of_ringHom_of_comp_eq (halg : IsAlgebraic S (g a)) (hf : Function.Surjective f) (hg : Function.Injective g)
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : IsAlgebraic R a :=
by
obtain ⟨p, h1, h2⟩ := halg
obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
refine ⟨q, fun h' ↦ by simp [h'] at h1, hg ?_⟩
change aeval ((g : A →+* B) a) _ = 0 at h2
change (g : A →+* B) _ = _
rw [map_zero, map_aeval_eq_aeval_map h, h2]
