stalkClosedPointTo_fromSpecStalk — Mathlib

English

For any x in X, the stalk-closed-point map at X.fromSpecStalk x equals the canonical stalk congruence homomorphism.

Русский

Для любой точки x в X карта stalkClosedPointTo от X.fromSpecStalk x равна каноническому гомоморфизму стежки.

LaTeX

$$$\\operatorname{stalkClosedPointTo}(X.fromSpecStalk x) = (X.presheaf.stalkCongr(\\text{proof})).hom$$$

Lean4

theorem stalkClosedPointTo_fromSpecStalk (x : X) :
    stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr (by rw [fromSpecStalk_closedPoint]; rfl)).hom :=
  by
  refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
  simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes]
  have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp
  convert germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU

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