mapHomologicalComplex_comp — Mathlib

English

Composition of natural transformations is preserved under mapHomologicalComplex: map(α ∘ β) = map α ∘ map β.

Русский

Сохранено сложение трансформаций: map(α ∘ β) = map α ∘ map β.

LaTeX

$$$\mathrm{mapHomologicalComplex}(c) (\alpha \circ \beta) = \mathrm{mapHomologicalComplex}(c) \alpha \circ \mathrm{mapHomological Complex}(c) \beta$$$

Lean4

@[simp]
theorem mapHomologicalComplex_comp (c : ComplexShape ι) {F G H : W₁ ⥤ W₂} [F.PreservesZeroMorphisms]
    [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (α : F ⟶ G) (β : G ⟶ H) :
    NatTrans.mapHomologicalComplex (α ≫ β) c =
      NatTrans.mapHomologicalComplex α c ≫ NatTrans.mapHomologicalComplex β c :=
  by cat_disch

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