arrowStalkMapIsoOfEq

Mathlib.AlgebraicGeometry.Scheme

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

Lean4

/-- If `x = y`, the stalk maps are isomorphic. -/
noncomputable def arrowStalkMapIsoOfEq {x y : X} (h : x = y) : Arrow.mk (f.stalkMap x) ≅ Arrow.mk (f.stalkMap y) :=
  Arrow.isoMk (Y.presheaf.stalkCongr <| (Inseparable.of_eq h).map f.continuous)
      (X.presheaf.stalkCongr <| Inseparable.of_eq h) <|
    by
    simp only [Arrow.mk_left, Arrow.mk_right, Functor.id_obj, TopCat.Presheaf.stalkCongr_hom, Arrow.mk_hom]
    rw [Scheme.stalkSpecializes_stalkMap]

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

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

Разделы

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

Аффилиация

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