toBasicOpen_to_map — Mathlib

English

The map toBasicOpen commutes with the canonical algebra map to localization via Away f.

Русский

Отображение toBasicOpen совместимо с естественным отображением в локализацию через Away f.

LaTeX

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

Lean4

@[simp]
theorem toBasicOpen_to_map (s f : R) :
    toBasicOpen R s (algebraMap R (Localization.Away s) f) =
      const R f 1 (PrimeSpectrum.basicOpen s) fun _ _ => Submonoid.one_mem _ :=
  (IsLocalization.lift_eq _ _).trans <|
    toOpen_eq_const _ _
      _
        -- The proof here follows the argument in Hartshorne's Algebraic Geometry, Proposition II.2.2.

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