coe_openToLocalization — Mathlib

English

The evaluation map openToLocalization is exactly the evaluation at x; as a function, it coincides with s ↦ s(x).

Русский

Функция openToLocalization совпадает с вычислением секции в точке x: s ↦ s(x).

LaTeX

$$$openToLocalization(R, U, x, hx) = \\lambda s . s(x).$$$

Lean4

@[simp]
theorem coe_openToLocalization (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
    (openToLocalization R U x hx : (structureSheaf R).1.obj (op U) → Localization.AtPrime x.asIdeal) = fun s =>
      s.1 ⟨x, hx⟩ :=
  rfl

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