mapHomologicalComplex — Mathlib

Lean4
/-- A natural isomorphism between functors induces a natural isomorphism
between those functors applied to homological complexes.
-/
@[simps!]
def mapHomologicalComplex {F G : W₁ ⥤ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G)
    (c : ComplexShape ι) : F.mapHomologicalComplex c ≅ G.mapHomologicalComplex c
    where
  hom := NatTrans.mapHomologicalComplex α.hom c
  inv := NatTrans.mapHomologicalComplex α.inv c
  hom_inv_id := by simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id, NatTrans.mapHomologicalComplex_id]
  inv_hom_id := by simp only [← NatTrans.mapHomologicalComplex_comp, α.inv_hom_id, NatTrans.mapHomologicalComplex_id]
Похожие утверждения