isMaximal_comap_C_of_isJacobsonRing

English

Under Jacobson hypothesis, the comap of a maximal ideal of R[X] is maximal in R.

Русский

При условии Якобсонова кольца, прообраз через C максимального идеала R[X] максимален в R.

LaTeX

$$(P.comap (C : R →+* R[X])).IsMaximal$$

Lean4

theorem isMaximal_comap_C_of_isJacobsonRing : (P.comap (C : R →+* R[X])).IsMaximal :=
  by
  rw [← @mk_ker _ _ P, RingHom.ker_eq_comap_bot, comap_comap]
  have := (bot_quotient_isMaximal_iff _).mpr hP
  exact isMaximal_comap_of_isIntegral_of_isMaximal' _ (quotient_mk_comp_C_isIntegral_of_isJacobsonRing P) ⊥

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