stalkToFiberLinearMap_toStalk — Mathlib

English

A precise equality expresses that the composition of the stalk-to-fiber map with the isomorphism to the stalk is the same as the localization at the prime ideal.

Русский

Точная равенство показывает, что композиция stalkToFiberLinearMap с изоморфизмом к стэку равна локализации по идеалу.

LaTeX

$$$(stalkToFiberLinearMap M x).hom (toStalk M x m) = LocalizedModule.mk m 1$$$

Lean4

theorem stalkToFiberLinearMap_toStalk (x : PrimeSpectrum.Top R) (m : M) :
    (stalkToFiberLinearMap M x).hom (toStalk M x m) = LocalizedModule.mk m 1 :=
  LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp (toStalk_comp_stalkToFiberLinearMap M x)) _

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