Singular cochains and singular cohomology

Let C be a k-linear abelian category with coproducts, and let R and M be objects of C. The singular cochain complex of a topological space X is obtained by applying the contravariant functor Hom(-, M) to the singular chain complex of X with coefficients in R: in degree n it is the k-module of morphisms Cₙ(X; R) ⟶ M, and its differential is precomposition with the singular boundary. Its cohomology is the singular cohomology of X. A continuous map f : X ⟶ Y induces a cochain map from the cochains of Y to those of X, precomposition with the chain map induced by f, so singular cohomology is a contravariant functor of the space.

For the usual cohomology of X with coefficients in a module M over a commutative ring k, take C := ModuleCat k and R := k: then Cₙ(X; k) is the free k-module on the singular n-simplices, and a cochain is a k-valued, respectively M-valued, function on them.

Main declarations

• TopCat.singularCochainComplex: the singular cochain complex of a space.
• TopCat.singularCochainComplexMap: the cochain map induced by a continuous map.
• TopCat.singularCohomology and TopCat.singularCohomologyMap: singular cohomology and the maps induced on it by continuous maps, with TauCeti.singularCohomologyFunctor the resulting functor TopCatᵒᵖ ⥤ ModuleCat k.
• SSet.constCochain: the constant 0-cochain with value e : R ⟶ M on every vertex of a simplicial set. TopCat.constSingularCocycle is the cocycle it defines for a space X. For e the unit of a ring of coefficients, its class is the unit of the cup product.

References

• A. Hatcher, Algebraic Topology, Section 3.1.

@[reducible, inline]

noncomputable abbrev TopCat.singularCochainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) : CochainComplex (ModuleCat k) ℕ

The singular cochain complex of a space X: in degree n, the k-module of morphisms from the singular n-chains of X with coefficients in R to M.

Equations

• TopCat.singularCochainComplex R k M X = ((TopCat.toSSet.obj X).chainComplex R).linearYonedaObj k M

@[reducible, inline]

noncomputable abbrev TopCat.singularCochainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y : TopCat} (f : X ⟶ Y) : singularCochainComplex R k M Y ⟶ singularCochainComplex R k M X

The cochain map on singular cochains induced by a continuous map f : X ⟶ Y: precomposition with the chain map induced by f.

Equations

• TopCat.singularCochainComplexMap f = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (SSet.chainComplexMap (TopCat.toSSet.map f) R).op

@[simp]

theorem TopCat.singularCochainComplexMap_f_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (g : ↑((singularCochainComplex R k M Y).X n)) : (CategoryTheory.ConcreteCategory.hom ((singularCochainComplexMap f).f n)) g = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (toSSet.map f) R).f n) g

The degree-n component of the cochain map induced by f acts by precomposition with the degree-n component of the induced singular chain map.

@[simp]

theorem TopCat.singularCochainComplexMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} (X : TopCat) : singularCochainComplexMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (singularCochainComplex R k M X)

theorem TopCat.singularCochainComplexMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : singularCochainComplexMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (singularCochainComplexMap g) (singularCochainComplexMap f)

theorem TopCat.singularCochainComplexMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : CochainComplex (ModuleCat k) ℕ} (h : singularCochainComplex R k M X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (singularCochainComplexMap (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (singularCochainComplexMap g) (CategoryTheory.CategoryStruct.comp (singularCochainComplexMap f) h)

@[reducible, inline]

noncomputable abbrev TopCat.singularCohomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) (n : ℕ) : ModuleCat k

The singular cohomology of a space X in degree n: the cohomology of the complex of morphisms from the singular chains of X with coefficients in R to M.

Equations

• TopCat.singularCohomology R k M X n = HomologicalComplex.homology (TopCat.singularCochainComplex R k M X) n

@[reducible, inline]

noncomputable abbrev TopCat.singularCohomologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : TopCat.singularCohomology R k M Y n ⟶ TopCat.singularCohomology R k M X n

The map on singular cohomology induced by a continuous map f : X ⟶ Y.

Equations

• TopCat.singularCohomologyMap f n = HomologicalComplex.homologyMap (TopCat.singularCochainComplexMap f) n

@[simp]

theorem TopCat.singularCohomologyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} (X : TopCat) (n : ℕ) : TopCat.singularCohomologyMap (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (TopCat.singularCohomology R k M X n)

theorem TopCat.singularCohomologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) : TopCat.singularCohomologyMap (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap g n) (TopCat.singularCohomologyMap f n)

theorem TopCat.singularCohomologyMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) {Z✝ : ModuleCat k} (h : TopCat.singularCohomology R k M X n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (CategoryTheory.CategoryStruct.comp f g) n) h = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap g n) (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f n) h)

noncomputable def TauCeti.singularCohomologyFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.Functor TopCatᵒᵖ (ModuleCat k)

Singular cohomology in degree n as a contravariant functor from topological spaces to k-modules.

Equations

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

@[simp]

theorem TauCeti.singularCohomologyFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) {X✝ Y✝ : TopCatᵒᵖ} (f : X✝ ⟶ Y✝) : (singularCohomologyFunctor R k M n).map f = TopCat.singularCohomologyMap f.unop n

@[simp]

theorem TauCeti.singularCohomologyFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) (X : TopCatᵒᵖ) : (singularCohomologyFunctor R k M n).obj X = TopCat.singularCohomology R k M (Opposite.unop X) n

noncomputable def SSet.constCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R M : C} (K : SSet) (e : R ⟶ M) : (K.chainComplex R).X 0 ⟶ M

The 0-cochain of a simplicial set K which takes the value e : R ⟶ M on every vertex.

Equations

• K.constCochain e = CategoryTheory.Limits.Cofan.IsColimit.desc (K.isColimitChainComplexXCofan R 0) fun (x : K.obj (Opposite.op { len := 0 })) => e

@[simp]

theorem SSet.ιChainComplex_constCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R M : C} (K : SSet) (e : R ⟶ M) (x : K.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (K.ιChainComplex x) (K.constCochain e) = e

The constant 0-cochain with value e takes the value e on every vertex.

@[simp]

theorem SSet.ιChainComplex_constCochain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R M : C} (K : SSet) (e : R ⟶ M) (x : K.obj (Opposite.op { len := 0 })) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιChainComplex x) (CategoryTheory.CategoryStruct.comp (K.constCochain e) h) = CategoryTheory.CategoryStruct.comp e h

The constant 0-cochain with value e takes the value e on every vertex.

@[simp]

theorem SSet.d_comp_constCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R M : C} (K : SSet) (e : R ⟶ M) : CategoryTheory.CategoryStruct.comp ((K.chainComplex R).d 1 0) (K.constCochain e) = 0

The constant 0-cochain is a cocycle: it takes the same value at both ends of an edge.

@[simp]

theorem SSet.d_comp_constCochain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R M : C} (K : SSet) (e : R ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.chainComplex R).d 1 0) (CategoryTheory.CategoryStruct.comp (K.constCochain e) h) = CategoryTheory.CategoryStruct.comp 0 h

The constant 0-cochain is a cocycle: it takes the same value at both ends of an edge.

noncomputable def TopCat.constSingularCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (e : R ⟶ M) : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) 0)

The constant 0-cochain (toSSet.obj X).constCochain e, as a cocycle.

Equations

• X.constSingularCocycle k e = HomologicalComplex.moduleCatCyclesMk (TopCat.singularCochainComplex R k M X) ((TopCat.toSSet.obj X).constCochain e) 1 TopCat.constSingularCocycle._proof_1✝ ⋯

@[simp]

theorem TopCat.iCycles_constSingularCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (e : R ⟶ M) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (singularCochainComplex R k M X) 0)) (X.constSingularCocycle k e) = (toSSet.obj X).constCochain e

The constant 0-cocycle has underlying cochain the constant 0-cochain.