Theorems · Definition · category theory

CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : CategoryTheory.SimplicialObject C} →
        {f g : X ⟶ Y} →
          CategoryTheory.SimplicialObject.Homotopy f g →
            Homotopy ((AlgebraicTopology.alternatingFaceMapComplex C).map f)
              ((AlgebraicTopology.alternatingFaceMapComplex C).map g)

A simplicial homotopy between f and g induces a chain homotopy between the induced morphisms on the alternating face map complexes.

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive