ofRestrict_app — Mathlib

English

The app map for restricted scheme X|h equals the map induced by presheaf restrict; i.e., (X.ofRestrict h).app V = X.presheaf.map (h.isOpenMap.adjunction.counit.app V).op.

Русский

Карта app ограниченного схемы X|h задаётся отображением из прешефа ограничений; равенство: (X.ofRestrict h).app V = X.presheaf.map (...).op.

LaTeX

$$$$ (X.ofRestrict h).app V = X.presheaf.map (h.isOpenMap.adjunction.counit.app V).op $$$$

Lean4

@[simp]
theorem ofRestrict_app (V) : (X.ofRestrict h).app V = X.presheaf.map (h.isOpenMap.adjunction.counit.app V).op :=
  rfl

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