comap_maximalIdeal — Mathlib

English

For an ideal J in Localization.AtPrime I, the comap equality to I occurs if and only if J equals the maximal ideal of Localization.AtPrime I.

Русский

Для идеала J в Localization.AtPrime I равенство comap с I имеет место тогда и только тогда, когда J равен максимальному идеалу Localization.AtPrime I.

LaTeX

$$$$ \operatorname{Ideal.comap}(\operatorname{algebraMap} R (Localization.AtPrime I)) J = I \;\Longleftrightarrow\; J = \operatorname{IsLocalRing.maximalIdeal}(Localization.AtPrime I) $$$$

Lean4

/-- The unique maximal ideal of the localization at `I.primeCompl` lies over the ideal `I`. -/
theorem comap_maximalIdeal :
    Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I :=
  IsLocalization.AtPrime.comap_maximalIdeal _ _

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