homeomorphOfRingEquiv — Mathlib

English

A ring isomorphism e: R ≃+* S induces a canonical homeomorphism between the prime spectra Spec(R) and Spec(S).

Русский

Кольцевой изоморфизм e: R ≃+* S порождает каноническое гомеоморфное отображение между спектрами Spec(R) и Spec(S).

LaTeX

$$homeomorphOfRingEquiv (e : R ≃+* S).$$

Lean4

/-- Homeomorphism between prime spectra induced by an isomorphism of semirings. -/
def homeomorphOfRingEquiv (e : R ≃+* S) : PrimeSpectrum R ≃ₜ PrimeSpectrum S
    where
  toFun := comap (e.symm : S →+* R)
  invFun := comap (e : R →+* S)
  left_inv _ := (comap_comp_apply ..).symm.trans (by simp)
  right_inv _ := (comap_comp_apply ..).symm.trans (by simp)

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