instHasFilteredColimitsOfSize — Mathlib

English

Equipping the HomologicalComplex with HasFilteredColimitsOfSize for any size, i.e., filtered colimits exist in the functor category of chain complexes.

Русский

Для категории, имеющей соответствующие ограниченности, у HomologicalComplex существуют отфильтрованные пределы заданного размера.

LaTeX

$$$ \\text{HasFilteredColimitsOfSize }(\\mathrm{HomologicalComplex} C c)$$$

Lean4

instance [HasFilteredColimitsOfSize.{w, w'} C] : HasFilteredColimitsOfSize.{w, w'} (HomologicalComplex C c) where
  HasColimitsOfShape J _ _ := by infer_instance

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