stalkMap_id

Mathlib.AlgebraicGeometry.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.stalkMap_id

English

The stalk map of the identity morphism evaluated at a point gives the identity on the stalk.

Русский

StalkMap тождества в точке дает тождество на stalk.

LaTeX

$$(\mathrm{id}).stalkMap x = 𝟙 (X.presheaf.stalk x)$$

Lean4

@[simp]
theorem stalkMap_id (X : Scheme.{u}) (x : X) : (𝟙 X : X ⟶ X).stalkMap x = 𝟙 (X.presheaf.stalk x) :=
  PresheafedSpace.stalkMap.id _ x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru