germ_comp_stalkToFiberRingHom — Mathlib

English

The germ map followed by the stalk-to-fiber map equals the localization map: the process of taking a germ and then passing to the fiber corresponds to evaluating at the localized stalk.

Русский

Герма карта, затем переход к волокну, равны локализации: взятие гермы и переход к волокну эквивалентны оценке в локализации.

LaTeX

$$$\\text{germ}_{U,x} \\, s \\;\\; \\circ \\; \\text{stalkToFiberRingHom}_x = openToLocalization(R, U, x, hx).$$$

Lean4

@[simp]
theorem germ_comp_stalkToFiberRingHom (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
    (structureSheaf R).presheaf.germ U x hx ≫ stalkToFiberRingHom R x = openToLocalization R U x hx :=
  Limits.colimit.ι_desc _ _

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