quotient_mk_comp_C_isIntegral_of_isJacobsonRing

English

There is a finite type isomorphism that preserves integrality after quotienting by P and mapping via C.

Русский

Существует изоморфизм, сохраняющий интегральность после факторирования по P и отображения через C.

LaTeX

$$IsIntegral((Ideal.Quotient.mk P).comp MvPolynomial.C)$$

Lean4

theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R]
    (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal] :
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) (MvPolynomial.C)) :=
  by
  change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
  apply quotient_mk_comp_C_isIntegral_of_isJacobsonRing'
  infer_instance

Похожие утверждения