toStalk_comp_stalkToFiberLinearMap

English

The composition toStalk M x with stalkToFiberLinearMap M x equals the canonical ofHom from Localization.

Русский

Состав toStalk M x и stalkToFiberLinearMap M x равен каноническому отображению from Localization.

LaTeX

$$toStalk M x ≫ stalkToFiberLinearMap M x = ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)$$

Lean4

@[reassoc (attr := simp)]
theorem toStalk_comp_stalkToFiberLinearMap (x : PrimeSpectrum.Top R) :
    toStalk M x ≫ stalkToFiberLinearMap M x = ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) := by
  rw [toStalk, Category.assoc, germ_comp_stalkToFiberLinearMap]; rfl

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