mapHomologicalComplex_naturality — Mathlib

English

The map on homological complexes of the identity natural transformation is the identity map on the mapped complex.

Русский

Отображение гомологических комплексов от тождественного преобразования равно тождественному отображению на отображённом комплексе.

LaTeX

$$$\mathrm{mapHomologicalComplex}(\mathrm{category.identity}\, F, c) = \mathrm{id}_{F.mapHomologicalComplex c}$$$

Lean4

@[reassoc]
theorem mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : W₁ ⥤ W₂} [F.PreservesZeroMorphisms]
    [G.PreservesZeroMorphisms] (α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) :
    (F.mapHomologicalComplex c).map f ≫ (NatTrans.mapHomologicalComplex α c).app D =
      (NatTrans.mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f :=
  by simp

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