mapShortComplex — Mathlib

English

If S is an exact short complex of functors X, then the map obtained by taking colimits is also exact, relative to chosen colimit cocones.

Русский

Если S — точный короткий комплекс из функторов X, то отображение, полученное взятием колимитов, также точное относительно выбранных коконтов колимита.

LaTeX

$$$\\text{ShortComplex}(S) \\text{ Exact } \\Rightarrow \\text{(mapShortComplex S)} \\text{Exact}$$$

Lean4

/-- Given `S : ShortComplex (J ⥤ C)` and (colimit) cocones for `S.X₁`, `S.X₂`,
`S.X₃` equipped with suitable data, this is the induced
short complex `c₁.pt ⟶ c₂.pt ⟶ c₃.pt`. -/
@[simps]
def mapShortComplex : ShortComplex C :=
  ShortComplex.mk f g
    (hc₁.hom_ext
      (fun j ↦ by
        dsimp
        rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero, zero_app, zero_comp]))

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