localization_toBasicOpen — Mathlib

English

The composite of the localization map with the structure sheaf map equals the basic open map: the localization through Away f is compatible with the open map to basicOpen f.

Русский

Состав локализации через Away f с отображением структуры sheaf совпадает с отображением к открытому множеству basicOpen f.

LaTeX

$$$toBasicOpen\\_toBasicOpen\\; =\\; toOpen\\; (R, basicOpen\\ f) \\circ algebraMap(R)(Away f).$$$

Lean4

@[simp]
theorem localization_toBasicOpen (f : R) :
    RingHom.comp (toBasicOpen R f) (algebraMap R (Localization.Away f)) = (toOpen R (PrimeSpectrum.basicOpen f)).hom :=
  RingHom.ext fun g => by rw [toBasicOpen, IsLocalization.Away.lift, RingHom.comp_apply, IsLocalization.lift_eq]

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