English
A prime ideal p in R is recovered by first mapping to S and then pulling back by f if and only if p is the restriction of a prime from S.
Русский
Простой идеал p в R восстанавливается отображением в S и взятием обратно по f тогда и только тогда, когда p является ограничением простого из S.
LaTeX
$$(p.map f).comap f = p ↔ ∃ q, q.IsPrime ∧ q.comap f = p$$
Lean4
/-- For a prime ideal `p` of `R`, `p` extended to `S` and
restricted back to `R` is `p` if and only if `p` is the restriction of a prime in `S`. -/
theorem comap_map_eq_self_iff_of_isPrime {S : Type*} [CommSemiring S] {f : R →+* S} (p : Ideal R) [p.IsPrime] :
(p.map f).comap f = p ↔ (∃ (q : Ideal S), q.IsPrime ∧ q.comap f = p) :=
by
refine ⟨fun hp ↦ ?_, ?_⟩
· obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _ (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃) (map_le_iff_le_comap.mp hq₂)⟩
· rintro ⟨q, hq, rfl⟩
simp
