restrict_top_presheaf — Mathlib

English

The morphism from the original presheafed space X to its restriction to the top subspace exists and has a canonical description.

Русский

Существует морфизм от X к его ограничению к верхней подпространстве, имеющий каноническое описание.

LaTeX

$$$X \to X.restrict(\mathrm{Opens.isOpenEmbedding}\;\top)$$$

Lean4

theorem restrict_top_presheaf (X : PresheafedSpace C) :
    (X.restrict (Opens.isOpenEmbedding ⊤)).presheaf = (Opens.inclusionTopIso X.carrier).inv _* X.presheaf :=
  by
  dsimp
  rw [Opens.inclusion'_top_functor X.carrier]
  rfl

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