English
If R is Jacobson, then there is a finite-type ring homomorphism from MvPolynomial to a field that is integral.
Русский
Если R — кольцо Якобсона, существует конечный тип гомоморфизма из MvPolynomial в поле, который интегрален.
LaTeX
$$IsIntegral((MvPolynomial.fin).comp C)$$
Lean4
theorem comp_C_integral_of_surjective_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R] {σ : Type*}
[Finite σ] {S : Type*} [Field S] (f : MvPolynomial σ R →+* S) (hf : Function.Surjective ↑f) :
(f.comp C).IsIntegral := by
cases nonempty_fintype σ
have e := (Fintype.equivFin σ).symm
let f' : MvPolynomial (Fin _) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
have hf' := Function.Surjective.comp hf (renameEquiv R e).surjective
change Function.Surjective ↑f' at hf'
have : (f'.comp C).IsIntegral :=
by
have : (RingHom.ker f').IsMaximal := ker_isMaximal_of_surjective f' hf'
let g : MvPolynomial _ R ⧸ (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 (fun r => rfl) fun i => 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'
rw [RingHom.comp_assoc] at this
convert this
refine RingHom.ext fun x => ?_
exact ((renameEquiv R e).commutes' x).symm
