instPreservesColimitsTopCatForgetOfHasLimits

English

If J has limits in the opposite sense and the shape is compatible with TopCat, then forgetful functor preserves colimits for shapes J in SheafedSpace.

Русский

Если у формы J есть пределы в противоположном виде и она совместима с TopCat, забывательная функтор сохраняет колимиты форм J в SheafedSpace.

LaTeX

$$$\forall J,\; [HasLimits (Opposite J)],\; \mathrm{PreservesColimits}(\mathrm{forget}\; C)$$$

Lean4

noncomputable instance [HasLimits C] : PreservesColimits (forget.{_, _, v} C) where

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