toRestrictTop — Mathlib

English

There is a canonical isomorphism between X and its restriction to the top subspace, given by toRestrictTop and restrictTopIso.

Русский

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

LaTeX

$$$\mathrm{restrictTopIso}(X): X.restrict(\mathrm{Opens.isOpenEmbedding}\;\top) \cong X$$$

Lean4

/-- The map to the restriction of a presheafed space along the canonical inclusion from the top
subspace.
-/
@[simps]
def toRestrictTop (X : PresheafedSpace C) : X ⟶ X.restrict (Opens.isOpenEmbedding ⊤)
    where
  base := (Opens.inclusionTopIso X.carrier).inv
  c := eqToHom (restrict_top_presheaf X)

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