Exactness of simplicial chains in the coefficients

Simplicial chains send a short exact sequence of coefficients to a short exact sequence of chain complexes whenever coproducts in the coefficient category are exact. The construction is Mathlib's SSet.chainComplexFunctor, whose degree-n object is a coproduct of coefficient objects over the n-simplices. Applying the homology long exact sequence gives the coefficient connecting homomorphisms, including Bockstein maps.

For rational coefficients, extension of scalars along the flat map ℤ → ℚ commutes with homology. SSet.rationalHomologyExtendScalarsIso compares rational extension of the integral homology with rational homology, on the native chain and module carriers. This fixed rational specialization needs no manifold, orientation, compactness or finite CW hypothesis.

References

• A. Hatcher, Algebraic Topology, Section 3.A, change of coefficients.

theorem CategoryTheory.ShortComplex.ShortExact.map_simplicialChains {C : Type u} [Category.{v, u} C] [Abelian C] [Limits.HasCoproducts C] [AB4OfSize.{w, v, u} C] {S : ShortComplex C} (hS : S.ShortExact) (X : SSet) : (S.map ((SSet.chainComplexFunctor C).flip.obj X)).ShortExact

Simplicial chains preserve short exact coefficient sequences when coproducts are exact.

instance ModuleCat.preservesFiniteLimits_extendScalars_intCastRat : CategoryTheory.Limits.PreservesFiniteLimits (extendScalars (Int.castRingHom ℚ))

Rational extension of scalars is exact, since ℚ is a localization of ℤ.

noncomputable def SSet.rationalHomologyExtendScalarsIso (X : SSet) (n : ℕ) : (ModuleCat.extendScalars (Int.castRingHom ℚ)).obj (X.homology (↧(ULift.{0, 0} ℤ)) n) ≅ X.homology (↧ℚ) n

Rational extension of integral simplicial homology is rational homology. The integral coefficient object is the native ULift ℤ; the rational coefficient object is ℚ.