under_map_of_isLocalizationAtPrime

English

The contraction of the localized extension is exactly the original ideal: contracting (p.map(algebraMap R S)) back to R yields p.

Русский

Сведение локализованного расширения обратно к R возвращает исходный идеал: конъюктирование (p.map(algebraMap R S)) обратно в R даёт p.

LaTeX

$$(p.map (algebraMap R S)).under R = p$$

Lean4

theorem under_map_of_isLocalizationAtPrime {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) :
    (p.map (algebraMap R S)).under R = p :=
  by
  have disj : Disjoint (q.primeCompl : Set R) p := by simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
  exact IsLocalization.comap_map_of_isPrime_disjoint _ _ p (by simpa) disj

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