Additivity of singular cochains and singular cohomology

The singular chains of a disjoint union form the coproduct of the singular chains of its summands. Applying the contravariant functor Hom(-, M) therefore identifies the singular cochain complex of the disjoint union with the product of the cochain complexes of the summands.

Products of modules over a ring are always exact, so taking cohomology preserves this product: the singular cohomology of a disjoint union is the product of the singular cohomologies of its summands. Both universal properties use the maps induced by the canonical inclusions into the disjoint union.

Main results

• TauCeti.isLimitFanSingularCochainComplex: singular cochains take a disjoint union to a product of cochain complexes.
• TauCeti.isLimitFanSingularCohomology: singular cohomology takes a disjoint union to a product in every degree.

Sources

The informal source is S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Chapter I, Section 3.

The coproduct decomposition of the singular chains is TauCeti.isColimitCofanSingularChainComplex, in TauCeti/AlgebraicTopology/Singular/Additivity, and the passage from cochains to cohomology is TauCeti.homologicalComplexHomologyFunctor_preservesLimitsOfShape, in TauCeti/Algebra/Homology/ShortComplex/Limit. The formal inputs from Mathlib are the linear Yoneda embedding linearYoneda and its comparison whiskering_linearYoneda with the ordinary Yoneda embedding, by Kim Morrison in Mathlib/CategoryTheory/Linear/Yoneda; the fact that Hom(-, M) takes coproducts to products, by Markus Himmel in Mathlib/CategoryTheory/Preadditive/Yoneda/Limits; the transfer of (co)limit preservation across opposite categories, by Markus Himmel in Mathlib/CategoryTheory/Limits/Preserves/Opposites and by Kim Morrison and Floris van Doorn in Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products; and the AB4* instance making products of abelian groups exact, by David Kurniadi Angdinata, Moritz Firsching, Nikolas Kuhn and Amelia Livingston in Mathlib/Algebra/Category/Grp/AB, from which exactness of products of modules is transferred along the forgetful functor.

noncomputable def TauCeti.isLimitFanSingularCochainComplex {ι : Type w} (X : ι → TopCat) (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{v, w} ι] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (TopCat.singularCochainComplex R k M ↧((i : ι) × ↑(X i))) fun (i : ι) => TopCat.singularCochainComplexMap (TopCat.sigmaι X i))

Additivity of singular cochains. The singular cochain complex of a disjoint union is the product of the singular cochain complexes of its summands. The projections are the cochain maps induced by the canonical inclusions of the summands.

Equations

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

noncomputable def TauCeti.isLimitFanSingularCohomology {ι : Type w} (X : ι → TopCat) (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{v, w} ι] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (TopCat.singularCohomology R k M (↧((i : ι) × ↑(X i))) n) fun (i : ι) => TopCat.singularCohomologyMap (TopCat.sigmaι X i) n)

Additivity of singular cohomology. In every degree, the singular cohomology of a disjoint union is the product of the singular cohomologies of its summands. The projections are the maps on cohomology induced by the canonical inclusions of the summands.

Equations

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