instPreservesColimitsOfShapeTopCatForget

English

For any J, the forgetful functor forgetting the presheafed-space structure to TopCat preserves colimits of shape J. That is, colimits computed in PresheafedSpace C become colimits after applying the forgetful functor.

Русский

Для любой формы J забывающая функция, переходящая из PresheafedSpace C к TopCat, сохраняет колимиты формы J: колимит в PresheafedSpace сохраняется после применения забывающей functor.

LaTeX

$$$\operatorname{forget}_C: \mathsf{PresheafedSpace}(C) \to \mathsf{TopCat} \text{ preserves colimits of shape } J$.$$

Lean4

instance : PreservesColimitsOfShape J (PresheafedSpace.forget.{u, v, v} C) :=
  ⟨fun {F} =>
    preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit F) <|
      by
      apply IsColimit.ofIsoColimit (colimit.isColimit _)
      fapply Cocones.ext
      · rfl
      · simp⟩

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