English
A prime p ∈ Spec R lies in the range of f.specComap iff (p.asIdeal.map f).comap f = p.asIdeal.
Русский
П_prime p в Spec R лежит в диапазоне f.specComap тогда и только тогда, когда (p.asIdeal.map f).comap f = p.asIdeal.
LaTeX
$$$p \\in \\operatorname{range} f.{\\rm specComap} \\iff (p.asIdeal.map f).comap f = p.asIdeal$$$
Lean4
/-- Let `f : R →+* S` be a surjective ring homomorphism, then `Spec S` is order-isomorphic to `Z(I)`
where `I = ker f`. -/
noncomputable def primeSpectrumOrderIsoZeroLocusOfSurj (hf : Surjective f) {I : Ideal R} (hI : RingHom.ker f = I) :
PrimeSpectrum S ≃o (PrimeSpectrum.zeroLocus (R := R) I)
where
toFun p := ⟨f.specComap p, hI.symm.trans_le (Ideal.ker_le_comap f)⟩
invFun := fun ⟨⟨p, _⟩, hp⟩ ↦ ⟨p.map f, p.map_isPrime_of_surjective hf (hI.trans_le hp)⟩
left_inv := by
intro ⟨p, _⟩
simp only [PrimeSpectrum.mk.injEq]
exact p.map_comap_of_surjective f hf
right_inv := by
intro ⟨⟨p, _⟩, hp⟩
simp only [Subtype.mk.injEq, PrimeSpectrum.mk.injEq]
exact (p.comap_map_of_surjective f hf).trans <| sup_eq_left.mpr (hI.trans_le hp)
map_rel_iff'
{a b} := by
change a.asIdeal.comap _ ≤ b.asIdeal.comap _ ↔ a ≤ b
rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf, PrimeSpectrum.asIdeal_le_asIdeal]
