stalkToFiberRingHom_localizationToStalk

English

The composition germ U x hx followed by stalkToFiberRingHom x equals openToLocalization.

Русский

Композиция germ U x hx затем stalkToFiberRingHom x равна openToLocalization.

LaTeX

$$$germ_{U,x} \\;\\circ\\; stalkToFiberRingHom_x = openToLocalization(R, U, x, hx).$$$

Lean4

@[simp, reassoc]
theorem stalkToFiberRingHom_localizationToStalk (x : PrimeSpectrum.Top R) :
    stalkToFiberRingHom R x ≫ localizationToStalk R x = 𝟙 _ :=
  (stalkIso R x).hom_inv_id

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