toStalk_stalkMap_toΓSpec — Mathlib

English

The map on stalks induced by the unit commutes with the stalk maps to Spec Γ(X).

Русский

Гомоморфизм локальных гомогенов на stalks композитивно согласуется с stalkMap.

LaTeX

$$$toStalk _ _ ≫ X.toΓSpecSheafedSpace.stalkMap x = X.presheaf.Γgerm x$$$

Lean4

/-- The map on stalks induced by the unit commutes with maps from `Γ(X)` to
stalks (in `Spec Γ(X)` and in `X`). -/
theorem toStalk_stalkMap_toΓSpec (x : X) : toStalk _ _ ≫ X.toΓSpecSheafedSpace.stalkMap x = X.presheaf.Γgerm x :=
  by
  rw [PresheafedSpace.Hom.stalkMap, ← toOpen_germ _ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial), ←
    Category.assoc, Category.assoc (toOpen _ _), stalkFunctor_map_germ, ← Category.assoc, X.toΓSpecSheafedSpace_app_eq,
    X.toΓSpecCApp_spec, Γgerm]
  erw [← stalkPushforward_germ _ _ X.presheaf ⊤]
  congr 1
  exact (X.toΓSpecBase _* X.presheaf).germ_res le_top.hom _ _

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