English
Equivalence: for J in Localization.AtPrime I, comap equality to I is equivalent to J being the maximal ideal.
Русский
Эквивалентность: для J в Localization.AtPrime I, равенство comap и I эквивалентно тому, что J является максимальным идеалом.
LaTeX
$$$$ \text{eq_maximalIdeal_iff_comap_eq} \;{J} : \operatorname{Ideal.comap}(\operatorname{algebraMap} R (Localization.AtPrime I)) J = I \iff J = \operatorname{IsLocalRing.maximalIdeal}(Localization.AtPrime I) $$$$
Lean4
theorem eq_maximalIdeal_iff_comap_eq {J : Ideal (Localization.AtPrime I)} :
Ideal.comap (algebraMap R (Localization.AtPrime I)) J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
where
mp
h :=
le_antisymm (IsLocalRing.le_maximalIdeal (fun hJ ↦ (hI.ne_top (h.symm ▸ hJ ▸ rfl)))) <| by
simpa [← AtPrime.map_eq_maximalIdeal, ← h] using Ideal.map_comap_le
mpr h := h.symm ▸ AtPrime.comap_maximalIdeal
