hasExactColimitsOfShape — Mathlib

English

If C has finite limits and filtered colimits of a given size, then the category of chain complexes has exact colimits of that shape.

Русский

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

LaTeX

$$$\text{HasExactColimitsOfShape } J (\mathrm{HomologicalComplex}\, C, c)$$$

Lean4

instance hasExactColimitsOfShape (J : Type w) [Category.{w'} J] [HasFiniteLimits C] [HasColimitsOfShape J C]
    [HasExactColimitsOfShape J C] : HasExactColimitsOfShape J (HomologicalComplex C c) where
  preservesFiniteLimits :=
    ⟨fun K _ _ ↦
      ⟨fun {F} ↦
        ⟨fun hc ↦
          ⟨isLimitOfEval _ _
              (fun i ↦ by
                let e := preservesColimitNatIso (J := J) (eval C c i)
                exact
                  (IsLimit.postcomposeHomEquiv (Functor.isoWhiskerLeft F e) _).1
                    (IsLimit.ofIsoLimit
                      (isLimitOfPreserves ((Functor.whiskeringRight J _ _).obj (eval C c i) ⋙ colim) hc)
                      (Cones.ext (e.symm.app _) (fun k ↦ (NatIso.naturality_2 e.symm _).symm))))⟩⟩⟩⟩

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