hasFilteredColimitsOfSize — Mathlib

English

There exist filtered colimits in the category of sheaves Sheaf J A, given HasSheafify and HasFilteredColimitsOfSize in A, etc.

Русский

В категории Sheaf J A существуют фильтрованные колимиты при наличии Sheafify и фильтрованных колимитов в A.

LaTeX

$$$\mathrm{HasFilteredColimitsOfSize}(\mathrm{Sheaf}\,J\,A)$$$

Lean4

instance hasFilteredColimitsOfSize [HasSheafify J A] [HasFilteredColimitsOfSize.{v₂, u₂} A] :
    HasFilteredColimitsOfSize.{v₂, u₂} (Sheaf J A) where HasColimitsOfShape K := by infer_instance

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