to_basicOpen_epi — Mathlib

English

For any r in R, the restriction map to the basic open basicOpen(r) is an epimorphism in the category of rings.

Русский

Для любого r в R отображение ограничения к базовому открытию basicOpen(r) является эпиморфизмом в категории колец.

LaTeX

$$$\\text{epi}\\ big(\\text{toOpen}(R, \\mathrm{basicOpen}(r))\\big)$$$

Lean4

instance to_basicOpen_epi (r : R) : Epi (toOpen R (PrimeSpectrum.basicOpen r)) :=
  ⟨fun _ _ h => CommRingCat.hom_ext (IsLocalization.ringHom_ext (Submonoid.powers r) (CommRingCat.hom_ext_iff.mp h))⟩

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