ab5OfSize — Mathlib

English

If C has filtered colimits of a given size and AB5 holds in C, then the corresponding category of chain complexes has AB5OfSize.

Русский

Если в C существуют фильтрованные колимиты заданного размера и выполняется AB5, то соответствующая категория комплексов имеет AB5OfSize.

LaTeX

$$$\mathrm{AB5OfSize}(C,c) \implies \mathrm{AB5OfSize}(\mathrm{CochainComplex}(C, c))$$$

Lean4

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

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