iso_inv_base_hom_base_apply

Mathlib.AlgebraicGeometry.Scheme

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

← MathLib Explorer

English

The stalk map of the identity morphism is the identity on the stalk.

Русский

Стalk карта для тождества равна тождественному отображению на stalk.

LaTeX

$$(\mathsf{id}).stalkMap = 𝟙$$

Lean4

@[simp]
theorem iso_inv_base_hom_base_apply {X Y : Scheme.{u}} (e : X ≅ Y) (y : Y) : (e.hom.base (e.inv.base y)) = y :=
  by
  change (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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