Theorems · Theorem · category theory

CategoryTheory.SimplicialObject.Homotopy.map_homology_eq

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} [inst_2 : CategoryTheory.CategoryWithHomology C]
  (H : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ),
  (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map
      ((AlgebraicTopology.alternatingFaceMapComplex C).map f) =
    (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map
      ((AlgebraicTopology.alternatingFaceMapComplex C).map g)

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomology