English
An isomorphism of rings induces an equivalence between the prime spectra, establishing a compatible order isomorphism.
Русский
Изоморфизм колец порождает эквивалентность между спектрами простых, сохраняющую порядок.
LaTeX
$$$\\text{comapEquiv}(e) : \\operatorname{PrimeSpectrum} R \\simeq_o \\operatorname{PrimeSpectrum} S$ for a ring isomorphism $e : R \\cong+* S$$$
Lean4
/-- `RingHom.specComap` of an isomorphism of rings as an equivalence of their prime spectra. -/
@[simps apply symm_apply]
def comapEquiv (e : R ≃+* S) : PrimeSpectrum R ≃o PrimeSpectrum S
where
toFun := e.symm.toRingHom.specComap
invFun := e.toRingHom.specComap
left_inv
x :=
by
rw [← specComap_comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp]
rfl
right_inv
x :=
by
rw [← specComap_comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm]
rfl
map_rel_iff' {I J} := Ideal.comap_le_comap_iff_of_surjective _ e.symm.surjective ..
