localization_away_isOpenEmbedding

English

The localization away from r induces an open embedding of PrimeSpectrum along comap(algebraMap R S).

Русский

Локализация Away(r) порождает открытое вложение спектра примитивных идеалов через comap(algebraMap).

LaTeX

$$$$ \\text{IsOpenEmbedding}(\\mathrm{comap}(\\mathrm{algebraMap}(R,S))). $$$$

Lean4

theorem localization_away_isOpenEmbedding (S : Type v) [CommSemiring S] [Algebra R S] (r : R)
    [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S))
    where
  toIsEmbedding := localization_comap_isEmbedding S (Submonoid.powers r)
  isOpen_range := by
    rw [localization_away_comap_range S r]
    exact isOpen_basicOpen

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