The simplicial chain complex preserves colimits

In degree n the chain complex of a simplicial set X with coefficients in an object R is the coproduct of copies of R indexed by the n-simplices of X. Evaluating a simplicial set in a fixed degree preserves colimits, because colimits of presheaves are computed pointwise, and forming a coproduct of copies of R preserves colimits; hence so does X ↦ X.chainComplex R.

The case of a coproduct is chain-level additivity: the chain complex of a disjoint union of simplicial sets is the coproduct of the chain complexes of the summands. The chain map induced by a monomorphism of simplicial sets is also a monomorphism.

Sources

The argument assembles three Mathlib constructions. The simplicial chain complex SSet.chainComplexFunctor and its degreewise cofan SSet.isColimitChainComplexXCofan are due to Joël Riou and Andrew Yang in Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic; the coproduct-of-copies functor CategoryTheory.Limits.sigmaConst and its colimit preservation are due to Joël Riou in Mathlib/CategoryTheory/Limits/Preserves/SigmaConst, as is the reduction of colimit preservation to the degreewise statement, HomologicalComplex.preservesColimitsOfShape_of_eval.

instance TauCeti.instPreservesColimitsOfShapeSSetChainComplexNatObjFunctorChainComplexFunctor_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {J : Type u'} [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type w)] : CategoryTheory.Limits.PreservesColimitsOfShape J ((SSet.chainComplexFunctor C).obj R)

The simplicial chain complex with coefficients in R preserves every shape of colimit that the category of w-small types has: in each degree it is the composite of evaluation, which preserves colimits of presheaves, with sigmaConst.obj R.

instance SSet.mono_chainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) [CategoryTheory.Mono f] : CategoryTheory.Mono (chainComplexMap f R)

The chain map induced by a monomorphism of simplicial sets is a monomorphism.