isGrothendieckAbelian — Mathlib

English

If C is abelian and Grothendieck abelian, then the category of chain complexes over C is Grothendieck abelian.

Русский

Если C — абелева категория и Гротендик-абелевая, то категория цепных комплексов над C тоже Гротендик-абелева.

LaTeX

$$$\mathrm{IsGrothendieckAbelian}(\mathrm{CochainComplex}(C,c))$$$

Lean4

instance isGrothendieckAbelian [Abelian C] [IsGrothendieckAbelian.{w} C] [c.HasNoLoop] [Small.{w} ι] :
    IsGrothendieckAbelian.{w} (HomologicalComplex C c) where
  hasSeparator :=
    by
    have : HasCoproductsOfShape ι C := hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{w} ι)).symm
    infer_instance

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