English
The pullback along an isomorphism of rings induces an equivalence of prime spectra; the pullback map is an order isomorphism between the prime spectra.
Русский
Тянуть обратно вдоль изоморфизма колец порождает эквиваленцию спектров простых, и отображение вытяжки является упорядоченным изоморфизмом между спектрами.
LaTeX
$$$\\mathrm{comapEquiv}(e) : \\operatorname{PrimeSpectrum} R \\simeq_o \\operatorname{PrimeSpectrum} S$ для изоморфизма колец $e : R \\cong+* S$$$
Lean4
/-- The pullback of an element of `PrimeSpectrum S` along a ring homomorphism `f : R →+* S`.
The bundled continuous version is `PrimeSpectrum.comap`. -/
abbrev specComap {R S : Type*} [CommSemiring R] [CommSemiring S] (f : R →+* S) : PrimeSpectrum S → PrimeSpectrum R :=
fun y => ⟨Ideal.comap f y.asIdeal, inferInstance⟩
