forget_preservesColimits — Mathlib

English

The forgetful functor from presheafed spaces to topological spaces preserves colimits.

Русский

Функтор забывания из прешефдов пространства в топологические пространства сохраняет колимиты.

LaTeX

$$$\mathsf{forget}\;: \mathrm{PresheafedSpace}\,C \to \mathrm{TopCat}$ preserves colimits.$$

Lean4

/-- The underlying topological space of a colimit of presheafed spaces is
the colimit of the underlying topological spaces.
-/
instance forget_preservesColimits [HasLimits C] : PreservesColimits (PresheafedSpace.forget.{_, _, v} C) where
  preservesColimitsOfShape
    {J
      𝒥} :=
    {
      preservesColimit := fun {F} =>
        preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit F)
          (IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Iso.refl _))) }

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