isMaximal_of_isIntegral_of_isMaximal_comap

English

Let I be a prime ideal in S, with I^comap via an integral extension maximal; then I is maximal in S as well.

Русский

Пусть I — простой идеал в S; если его обратный образ по интегральному расширению максимален, тогда и сам I максимален.

LaTeX

$$$$\text{IsMaximal}(I^{\mathrm{comap} \; f}) \Rightarrow \text{IsMaximal}(I).$$$$

Lean4

theorem isMaximal_of_isIntegral_of_isMaximal_comap [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) [I.IsPrime]
    (hI : IsMaximal (I.comap (algebraMap R S))) : IsMaximal I :=
  ⟨⟨mt comap_eq_top_iff.mpr hI.1.1, fun _ I_lt_J =>
      let ⟨I_le_J, x, hxJ, hxI⟩ := SetLike.lt_iff_le_and_exists.mp I_lt_J
      comap_eq_top_iff.1 <|
        hI.1.2 _ (comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩ (Algebra.IsIntegral.isIntegral x))⟩⟩

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