Theorems · Definition · category theory

HomologicalComplex.Hom.isoOfComponents

{ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          {C₁ C₂ : HomologicalComplex V c} →
            (f : (i : ι) → C₁.X i ≅ C₂.X i) →
              autoParam
                  (∀ (i j : ι),
                    c.Rel i j →
                      CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
                        CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom)
                  HomologicalComplex.Hom.isoOfComponents._auto_1 →
                (C₁ ≅ C₂)

Construct an isomorphism of chain complexes from isomorphism of the objects which commute with the differentials.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

5 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms