height_comap — Mathlib

English

For a localization S → A and a prime ideal J in A, the comap under algebra map has the same primeHeight as J.

Русский

Для локализации и простого идеала J в A высота простого идеала после комапа по алгебраическому отображению равна высоте J.

LaTeX

$$$\operatorname{primeHeight}(J \downarrow) = \operatorname{primeHeight}(J).$$$

Lean4

theorem height_comap (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A] [IsLocalization S A] (J : Ideal A) :
    (J.comap (algebraMap R A)).height = J.height :=
  by
  rw [Ideal.height, Ideal.height]
  simp_rw [← IsLocalization.primeHeight_comap S, IsLocalization.minimalPrimes_comap S A, ← Ideal.height_eq_primeHeight,
    iInf_image]

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