Additivity of singular chains and singular homology

A singular simplex of a disjoint union Σ i, X i has connected domain, so its image lies in a single summand, and it comes from a singular simplex of that summand in exactly one way. Hence the singular simplicial set of a disjoint union is the coproduct of the singular simplicial sets of the summands, and, since the simplicial chain complex functor preserves colimits, so is the singular chain complex.

Passing to homology needs one more input: homology commutes with the coproduct of chain complexes when coproducts are exact in the coefficient category (Grothendieck's axiom AB4, as for modules over a ring). Under that hypothesis the singular homology of a disjoint union is the coproduct of the singular homologies of the summands in every degree. This is the additivity axiom of Eilenberg--Steenrod.

The same holds for relative singular chains and relative singular homology of the disjoint union TopPair.sigma P = ∐ᵢ (Xᵢ, Aᵢ) of a family of topological pairs: relative chains are the cokernel of the map from the chains of the subspace to those of the ambient space, both of which are additive, and cokernels commute with coproducts.

Every map in sight is induced by one of the inclusions X i ⟶ Σ i, X i, so the results are statements about cofans rather than unrelated degreewise decompositions.

Main results

• TauCeti.isColimitCofanSingularChainComplex: the singular chain complex of Σ i, X i is the coproduct of the singular chain complexes of the X i.
• TauCeti.isColimitCofanSingularHomology: if coproducts indexed by ι are exact in the coefficient category, the singular homology of Σ i, X i in each degree is the coproduct of the singular homologies of the X i.
• TopPair.isColimitCofanSingularChainComplex and TopPair.isColimitCofanSingularHomology: the same for the relative singular chains and relative singular homology of ∐ᵢ (Xᵢ, Aᵢ).

Sources

The informal source is Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III. The connectedness argument is Mathlib's ContinuousMap.sigmaCodHomeomorph, by Yury Kudryashov in Mathlib/Topology/ContinuousMap/Sigma; the singular simplicial set TopCat.toSSet and the singular chain complex AlgebraicTopology.singularChainComplexFunctor are by Andrew Yang in Mathlib/AlgebraicTopology/SingularHomology/Basic, building on Joël Riou's TopCat.toSSet adjunction; and the concrete cofan TopCat.sigmaCofanIsColimit is by Patrick Massot, Kim Morrison, Mario Carneiro and Andrew Yang in Mathlib/Topology/Category/TopCat/Limits/Products. The passage from chains to homology is TauCeti.homologicalComplexHomologyFunctor_preservesColimitsOfShape, in TauCeti/Algebra/Homology/ShortComplex/Colimit, applied with Mathlib's exactness class HasExactColimitsOfShape. The passage from absolute to relative chains is TauCeti.isColimitCofanMkCokernelCofork, in TauCeti/CategoryTheory/Limits/Shapes/Products.

theorem TauCeti.toSSet_map_sigmaι_app_bijective {ι : Type w} (X : ι → TopCat) (n : SimplexCategoryᵒᵖ) : Function.Bijective fun (p : (i : ι) × (TopCat.toSSet.obj (X i)).obj n) => (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map (TopCat.sigmaι X p.fst)).app n)) p.snd

In each degree, the singular simplices of a disjoint union of spaces are exactly the singular simplices of the summands: the topological simplex is connected, so a singular simplex of Σ i, X i comes from a unique summand and a unique singular simplex there.

noncomputable def TauCeti.isColimitCofanToSSetObj {ι : Type w} (X : ι → TopCat) (n : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk ((TopCat.toSSet.obj ↧((i : ι) × ↑(X i))).obj n) fun (i : ι) => (TopCat.toSSet.map (TopCat.sigmaι X i)).app n)

In each degree, the singular simplices of a disjoint union form the coproduct of the singular simplices of the summands.

Equations

• TauCeti.isColimitCofanToSSetObj X n = ⋯.some

instance TauCeti.instPreservesColimitsOfShapeTopCatSSetDiscreteToSSet_tauCeti {ι : Type w} : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) TopCat.toSSet

The singular simplicial set functor preserves coproducts of families indexed by ι.

noncomputable def TauCeti.isColimitCofanToSSet {ι : Type w} (X : ι → TopCat) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (TopCat.toSSet.obj ↧((i : ι) × ↑(X i))) fun (i : ι) => TopCat.toSSet.map (TopCat.sigmaι X i))

The singular simplicial set of a disjoint union of spaces is the coproduct of the singular simplicial sets of the summands.

Equations

• TauCeti.isColimitCofanToSSet X = CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit TopCat.toSSet X (TopCat.sigmaι X) (TopCat.sigmaCofanIsColimit X)

instance TauCeti.instPreservesColimitsOfShapeTopCatChainComplexNatDiscreteObjFunctorSingularChainComplexFunctor_tauCeti {ι : Type w} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) ((AlgebraicTopology.singularChainComplexFunctor C).obj R)

The singular chain complex with coefficients in R preserves coproducts of families indexed by ι: it is the singular simplicial set functor followed by the simplicial chain complex functor, and both preserve them.

noncomputable def TauCeti.isColimitCofanSingularChainComplex {ι : Type w} (X : ι → TopCat) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧((i : ι) × ↑(X i))) fun (i : ι) => ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.sigmaι X i))

Additivity of singular chains. The singular chain complex of a disjoint union of spaces, with coefficients in R, is the coproduct of the singular chain complexes of the summands, with the inclusions of the summands as the cofan legs.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.instPreservesColimitsOfShapeTopCatDiscreteObjFunctorSingularHomologyFunctor_tauCeti {ι : Type w} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ι) C] (R : C) (k : ℕ) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) ((AlgebraicTopology.singularHomologyFunctor C k).obj R)

Singular homology in each degree, with coefficients in R, preserves coproducts of families indexed by ι when such coproducts are exact in C: it is the singular chain complex followed by homology, and both preserve them.

noncomputable def TauCeti.isColimitCofanSingularHomology {ι : Type w} (X : ι → TopCat) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ι) C] (R : C) (k : ℕ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (((AlgebraicTopology.singularHomologyFunctor C k).obj R).obj ↧((i : ι) × ↑(X i))) fun (i : ι) => ((AlgebraicTopology.singularHomologyFunctor C k).obj R).map (TopCat.sigmaι X i))

Additivity of singular homology. If coproducts indexed by ι are exact in C, then in every degree the singular homology of a disjoint union of spaces, with coefficients in R, is the coproduct of the singular homologies of the summands, with the maps induced by the inclusions of the summands as the cofan legs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TopPair.isColimitCofanSingularChainComplex {ι : Type w} (P : ι → TopPair) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk ((sigma P).singularChainComplex R) fun (i : ι) => singularChainComplexMap (sigmaι P i) R)

Additivity of relative singular chains. The relative singular chain complex of the disjoint union ∐ᵢ (Xᵢ, Aᵢ) of a family of topological pairs, with coefficients in R, is the coproduct of the relative singular chain complexes of the pairs, with the inclusions of the summands as the cofan legs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TopPair.isColimitCofanSingularHomology {ι : Type w} (P : ι → TopPair) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ι) C] (R : C) (k : ℕ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk ((sigma P).singularHomology R k) fun (i : ι) => TopPair.singularHomologyMap (sigmaι P i) R k)

Additivity of relative singular homology. If coproducts indexed by ι are exact in C, then in every degree the relative singular homology of the disjoint union ∐ᵢ (Xᵢ, Aᵢ) of a family of topological pairs, with coefficients in R, is the coproduct of the relative singular homologies of the pairs, with the maps induced by the inclusions of the summands as the cofan legs.

Equations

• One or more equations did not get rendered due to their size.