instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite

English

For a presheafed space X and an open embedding h, the inverse of the stalk-isomorphism coming from restricting X equals the stalk map of X restricted along h.

Русский

Для X и открытого встраивания h обратная стенка из restrictStalkIso равна stalkMap для ограниченного X.

LaTeX

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

Lean4

instance (J : Type w) [Category.{w'} J] [Small.{v} J] [HasLimitsOfShape Jᵒᵖ C] :
    HasColimitsOfShape J (SheafedSpace.{_, _, v} C) :=
  hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape forgetToPresheafedSpace

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