Singular chain complexes

This module relates the singular-chain functor to the chain map induced by a map of singular simplicial sets.

@[simp]

theorem TauCeti.singularChainComplexFunctor_obj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {X Y : TopCat} (f : X ⟶ Y) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f = SSet.chainComplexMap (TopCat.toSSet.map f) R

The singular chain complex functor with coefficients in R sends a continuous map f to the simplicial chain map induced by the singular simplicial map TopCat.toSSet.map f.

@[simp]

theorem TauCeti.singularChainComplexFunctor_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R R' : C} (g : R ⟶ R') (X : TopCat) : ((AlgebraicTopology.singularChainComplexFunctor C).map g).app X = ((SSet.chainComplexFunctor C).map g).app (TopCat.toSSet.obj X)

A coefficient morphism acts on singular chains by its simplicial chain map evaluated at the singular simplicial set.