id — Mathlib · SciLib

English

Re-states the equality of the stalk iso inverse with the ofRestrict stalk map, reinforcing the identifications under restriction.

Русский

Повторяет равенство и обратной restrictStalkIso с stalkMap от restricт.

LaTeX

$$$(X.ofRestrict h).stalkMap x = (restrictStalkIso\,h\,x)^{-1}$$$

Lean4

@[simp]
theorem id (X : PresheafedSpace.{_, _, v} C) (x : X) : (𝟙 X : X ⟶ X).stalkMap x = 𝟙 (X.presheaf.stalk x) :=
  by
  dsimp [Hom.stalkMap]
  simp only [stalkPushforward.id]
  rw [← map_comp]
  convert (stalkFunctor C x).map_id X.presheaf
  ext
  simp only [id_c, id_comp, Pushforward.id_hom_app]
  rfl

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