English
If a surjective RingHom f: R[X] → S has kernel maximal, the induced map from the quotient by the kernel composes to an integral map, giving IsIntegral of the composed map with C.
Русский
Если ядро гомоморфа f максимальное, композиция с C образует интегральный отображение.
LaTeX
$$$(f \\circ C).IsIntegral$$$
Lean4
theorem comp_C_integral_of_surjective_of_isJacobsonRing {S : Type*} [Field S] (f : R[X] →+* S)
(hf : Function.Surjective ↑f) : (f.comp C).IsIntegral :=
by
have : (RingHom.ker f).IsMaximal := RingHom.ker_isMaximal_of_surjective f hf
let g : R[X] ⧸ (RingHom.ker f) →+* S := Ideal.Quotient.lift (RingHom.ker f) f fun _ h => h
have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f := ringHom_ext' rfl rfl
rw [← hfg, RingHom.comp_assoc]
refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f)).trans _ g (g.isIntegral_of_surjective ?_)
rw [← hfg] at hf
norm_num at hf
exact Function.Surjective.of_comp hf
