Theorems · Definition · category theory

CochainComplex.HomComplex.Cochain.map

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          {D : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_1, u_2} D] →
              [inst_3 : CategoryTheory.Preadditive D] →
                CochainComplex.HomComplex.Cochain K L n →
                  (Φ : CategoryTheory.Functor C D) →
                    [inst_4 : Φ.Additive] →
                      CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)
                        ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n

If Φ : C ⥤ D is an additive functor, a cochain z : Cochain K L n between cochain complexes in C can be mapped to a cochain between the cochain complexes in D obtained by applying the functor Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Functor.Additive