The singular cohomology of the base of a contractible free cover is group cohomology

Let p : E ⟶ B be the quotient covering map of an action of a group G on E, in the sense of Mathlib's IsQuotientCoveringMap, let k be a commutative ring and let M be a k-module. An M-valued singular n-cochain f of B pulls back to the cochain f ∘ p_* of E, which is invariant under G, that is, a morphism from the representation TauCeti.singularChainsRepresentation k E G n to the trivial representation on M. Every G-invariant cochain of E arises in this way from exactly one cochain of B, because every singular simplex of B lifts to E and two lifts differ by an element of G. So the singular cochains of B are the complex Hom_G(C(E; k), M) (IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj).

If E is contractible, the singular chains of E are a projective resolution of the trivial representation k (TauCeti.singularChainsResolution). Group cohomology is the cohomology of Hom_G(P, M) for any projective resolution P of k (groupCohomologyIso), so the singular cohomology of B with coefficients in M is the group cohomology of G with coefficients in the trivial representation M (IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology):

Hⁿ(B; M) ≅ Hⁿ(G, M).

Both identifications are natural in the coefficients: postcomposing cochains with a linear map f : M →ₗ[k] N corresponds to Mathlib's map groupCohomology.map (MonoidHom.id G) induced by f on trivial representations (IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology_hom_naturality).

Both identifications are also natural for maps of quotient covers equivariant along arbitrary group homomorphisms. For a map b : B ⟶ C of bases covered by a map f : E ⟶ F of total spaces equivariant along φ : G →* H, pulling cochains back along b corresponds to the cochain map u ↦ f_* ≫ u on invariant cochains of the total spaces (singularCochainComplexMap_comp_singularCochainComplexIsoLinearYonedaObj_hom, in the namespace IsQuotientCoveringMap), and, for contractible total spaces, b^* on singular cohomology corresponds to Mathlib's change-of-group map groupCohomology.map φ with the identity on the trivial coefficients M (IsQuotientCoveringMap.singularCohomologyMap_comp_singularCohomologyIsoGroupCohomology_hom). No hypothesis on φ is needed.

The identification also respects the long exact sequences in the coefficients. A short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of k-modules is a short exact sequence of trivial representations, and for contractible E the isomorphisms Hⁿ(B; Mᵢ) ≅ Hⁿ(G, Mᵢ) carry the Bockstein homomorphism Hⁿ(B; M₃) ⟶ Hⁿ⁺¹(B; M₁) of singular cohomology to Mathlib's connecting map groupCohomology.δ of group cohomology (IsQuotientCoveringMap.singularCohomologyBockstein_comp_singularCohomologyIsoGroupCohomology_hom). The comparison of cochains is natural in the coefficients, so it is a morphism of short exact sequences of cochain complexes, and groupCohomologyIso intertwines the connecting maps (TauCeti.Rep.δ_comp_groupCohomologyIso_inv).

This is the cohomological counterpart of IsQuotientCoveringMap.singularHomologyIsoGroupHomology.

Main definitions

• IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj: the singular cochains of B are the G-invariant cochains of E.
• IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology: for contractible E, the singular cohomology of B is the group cohomology of G with trivial coefficients.

Main results

• IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_hom_f_hom_apply: the comparison of cochains is pulling back along p.
• IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_inv_f_hom_apply: its inverse descends an invariant cochain of E along p.
• IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_hom_naturality, IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology_hom_naturality: the comparisons of cochains and of cohomology are natural in the coefficients.
• singularCochainComplexMap_comp_singularCochainComplexIsoLinearYonedaObj_hom, IsQuotientCoveringMap.singularCohomologyMap_comp_singularCohomologyIsoGroupCohomology_hom: the comparisons of cochains and of cohomology are natural in the covering and the group.
• IsQuotientCoveringMap.singularCohomologyBockstein_comp_singularCohomologyIsoGroupCohomology_hom: the comparison of cohomology carries the Bockstein homomorphism to the connecting map of group cohomology.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Section II.4, Section III.1, and Section III.8.

noncomputable def IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] : TopCat.singularCochainComplex (↧k) k (↧M) B ≅ (TauCeti.singularChainsRep k E G).linearYonedaObj k (Rep.trivial k G M)

The singular cochains of the base of a quotient covering are the invariant cochains of the total space: for the quotient covering map p : E ⟶ B of an action of G, pulling back along p is an isomorphism from the complex of M-valued singular cochains of B to the complex Hom_G(C(E; k), M) of morphisms to the trivial representation M.

@[simp]

theorem IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_hom_f_hom_apply {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] (n : ℕ) (f : ((TauCeti.singularChains k).obj B).X n ⟶ ↧M) (c : ↑(((TauCeti.singularChains k).obj E).X n)) : (Rep.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((hG.singularCochainComplexIsoLinearYonedaObj k M).hom.f n)) f)) c = (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (((TauCeti.singularChains k).map p).f n)) c)

The comparison of cochains pulls an M-valued cochain f of the base back to the cochain f ∘ p_* of the total space.

theorem IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_inv_f_hom_apply {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] (n : ℕ) (c : ↑(((TauCeti.singularChains k).obj E).X n)) (f : Rep.of (TauCeti.singularChainsRepresentation k E G n) ⟶ Rep.trivial k G M) : (ModuleCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((hG.singularCochainComplexIsoLinearYonedaObj k M).inv.f n)) f)) ((CategoryTheory.ConcreteCategory.hom (((TauCeti.singularChains k).map p).f n)) c) = (Rep.Hom.hom f) c

The inverse comparison descends a G-invariant cochain f of the total space to the cochain of the base whose value on the image p_* c of a chain c is f c.

theorem IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_hom_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {N : Type u} [AddCommGroup N] [Module k N] (f : M →ₗ[k] N) : CategoryTheory.CategoryStruct.comp (ChainComplex.linearYonedaObjMap k ((TauCeti.singularChains k).obj B) (ModuleCat.ofHom f)) (hG.singularCochainComplexIsoLinearYonedaObj k N).hom = CategoryTheory.CategoryStruct.comp (hG.singularCochainComplexIsoLinearYonedaObj k M).hom (ChainComplex.linearYonedaObjMap k (TauCeti.singularChainsRep k E G) ((Rep.trivialFunctor k G).map (ModuleCat.ofHom f)))

The comparison of cochains is natural in the coefficients: postcomposing an M-valued cochain of the base with a linear map f : M →ₗ[k] N and then pulling back along p is pulling back first and then postcomposing with f, viewed as a morphism of trivial representations.

theorem IsQuotientCoveringMap.singularCochainComplexIsoLinearYonedaObj_hom_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {N : Type u} [AddCommGroup N] [Module k N] (f : M →ₗ[k] N) {Z : CochainComplex (ModuleCat k) ℕ} (h : (TauCeti.singularChainsRep k E G).linearYonedaObj k (Rep.trivial k G N) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ChainComplex.linearYonedaObjMap k ((TauCeti.singularChains k).obj B) (ModuleCat.ofHom f)) (hG.singularCochainComplexIsoLinearYonedaObj k N).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (hG.singularCochainComplexIsoLinearYonedaObj k M).hom (ChainComplex.linearYonedaObjMap k (TauCeti.singularChainsRep k E G) ((Rep.trivialFunctor k G).map (ModuleCat.ofHom f)))) h

The comparison of cochains is natural in the coefficients: postcomposing an M-valued cochain of the base with a linear map f : M →ₗ[k] N and then pulling back along p is pulling back first and then postcomposing with f, viewed as a morphism of trivial representations.

noncomputable def IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] [ContractibleSpace ↑E] (n : ℕ) : TopCat.singularCohomology (↧k) k (↧M) B n ≅ groupCohomology (Rep.trivial k G M) n

The singular cohomology of the base of a contractible free covering is group cohomology: for the quotient covering map p : E ⟶ B of an action of G with contractible total space, the singular cohomology Hⁿ(B; M) with coefficients in a k-module M is Mathlib's group cohomology Hⁿ(G, M) of the trivial representation M. The singular chains of E form a free resolution of k over k[G], whose G-invariant M-valued cochains are the singular cochains of B.

theorem IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology_hom_eq {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] [ContractibleSpace ↑E] (n : ℕ) : (hG.singularCohomologyIsoGroupCohomology k M n).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hG.singularCochainComplexIsoLinearYonedaObj k M).hom n) (groupCohomologyIso (Rep.trivial k G M) n (TauCeti.singularChainsResolution k E G)).inv

The comparison Hⁿ(B; M) ≅ Hⁿ(G, M) is the cohomology of the comparison of cochains followed by the inverse of groupCohomologyIso for the resolution by singular chains of E.

theorem IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology_hom_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {N : Type u} [AddCommGroup N] [Module k N] [ContractibleSpace ↑E] (f : M →ₗ[k] N) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((TauCeti.singularChains k).obj B) (ModuleCat.ofHom f)) n) (hG.singularCohomologyIsoGroupCohomology k N n).hom = CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k M n).hom (groupCohomology.map (MonoidHom.id G) ((Rep.trivialFunctor k G).map (ModuleCat.ofHom f)) n)

The comparison of singular cohomology with group cohomology is natural in the coefficients: for the quotient covering map p : E ⟶ B of an action of G with contractible total space and a k-linear map f : M →ₗ[k] N, the isomorphisms Hⁿ(B; M) ≅ Hⁿ(G, M) and Hⁿ(B; N) ≅ Hⁿ(G, N) carry the map on singular cohomology induced by postcomposing cochains with f to Mathlib's map groupCohomology.map (MonoidHom.id G) induced by f on trivial representations.

theorem IsQuotientCoveringMap.singularCohomologyIsoGroupCohomology_hom_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {N : Type u} [AddCommGroup N] [Module k N] [ContractibleSpace ↑E] (f : M →ₗ[k] N) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology (Rep.trivial k G N) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((TauCeti.singularChains k).obj B) (ModuleCat.ofHom f)) n) (hG.singularCohomologyIsoGroupCohomology k N n).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k M n).hom (groupCohomology.map (MonoidHom.id G) ((Rep.trivialFunctor k G).map (ModuleCat.ofHom f)) n)) h

The comparison of singular cohomology with group cohomology is natural in the coefficients: for the quotient covering map p : E ⟶ B of an action of G with contractible total space and a k-linear map f : M →ₗ[k] N, the isomorphisms Hⁿ(B; M) ≅ Hⁿ(G, M) and Hⁿ(B; N) ≅ Hⁿ(G, N) carry the map on singular cohomology induced by postcomposing cochains with f to Mathlib's map groupCohomology.map (MonoidHom.id G) induced by f on trivial representations.

theorem IsQuotientCoveringMap.singularCochainComplexMap_comp_singularCochainComplexIsoLinearYonedaObj_hom {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) : CategoryTheory.CategoryStruct.comp (TopCat.singularCochainComplexMap b) (hG.singularCochainComplexIsoLinearYonedaObj k M).hom = CategoryTheory.CategoryStruct.comp (hH.singularCochainComplexIsoLinearYonedaObj k M).hom (φ.linearYonedaObjMap (CategoryTheory.CategoryStruct.id (Rep.trivial k G M)) (TauCeti.singularChainsRepResMap k f hf))

The comparison of cochains is natural for maps of quotient covers. For quotient covers p : E ⟶ B and q : F ⟶ C, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, pulling an M-valued cochain of C back along b and then along p is pulling it back along q and then along f, viewed as the change-of-group map MonoidHom.linearYonedaObjMap of invariant cochains with the identity on the trivial coefficients M.

theorem IsQuotientCoveringMap.singularCochainComplexMap_comp_singularCochainComplexIsoLinearYonedaObj_hom_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) {Z : CochainComplex (ModuleCat k) ℕ} (h : (TauCeti.singularChainsRep k E G).linearYonedaObj k (Rep.trivial k G M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.singularCochainComplexMap b) (CategoryTheory.CategoryStruct.comp (hG.singularCochainComplexIsoLinearYonedaObj k M).hom h) = CategoryTheory.CategoryStruct.comp (hH.singularCochainComplexIsoLinearYonedaObj k M).hom (CategoryTheory.CategoryStruct.comp (φ.linearYonedaObjMap (CategoryTheory.CategoryStruct.id (Rep.trivial k G M)) (TauCeti.singularChainsRepResMap k f hf)) h)

The comparison of cochains is natural for maps of quotient covers. For quotient covers p : E ⟶ B and q : F ⟶ C, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, pulling an M-valued cochain of C back along b and then along p is pulling it back along q and then along f, viewed as the change-of-group map MonoidHom.linearYonedaObjMap of invariant cochains with the identity on the trivial coefficients M.

theorem IsQuotientCoveringMap.singularCohomologyMap_comp_singularCohomologyIsoGroupCohomology_hom {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) [ContractibleSpace ↑E] [ContractibleSpace ↑F] (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap b n) (hG.singularCohomologyIsoGroupCohomology k M n).hom = CategoryTheory.CategoryStruct.comp (hH.singularCohomologyIsoGroupCohomology k M n).hom (groupCohomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G M)) n)

The comparison of singular cohomology with group cohomology is natural in the covering and the group. For quotient covers p : E ⟶ B and q : F ⟶ C with contractible total spaces, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, the identifications Hⁿ(C; M) ≅ Hⁿ(H, M) and Hⁿ(B; M) ≅ Hⁿ(G, M) carry b^* to Mathlib's change-of-group map groupCohomology.map φ, with the identity on the trivial coefficients M.

theorem IsQuotientCoveringMap.singularCohomologyMap_comp_singularCohomologyIsoGroupCohomology_hom_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (M : Type u) [AddCommGroup M] [Module k M] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) [ContractibleSpace ↑E] [ContractibleSpace ↑F] (n : ℕ) {Z : ModuleCat k} (h : groupCohomology (Rep.trivial k G M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap b n) (CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k M n).hom h) = CategoryTheory.CategoryStruct.comp (hH.singularCohomologyIsoGroupCohomology k M n).hom (CategoryTheory.CategoryStruct.comp (groupCohomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G M)) n) h)

The comparison of singular cohomology with group cohomology is natural in the covering and the group. For quotient covers p : E ⟶ B and q : F ⟶ C with contractible total spaces, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, the identifications Hⁿ(C; M) ≅ Hⁿ(H, M) and Hⁿ(B; M) ≅ Hⁿ(G, M) carry b^* to Mathlib's change-of-group map groupCohomology.map φ, with the identity on the trivial coefficients M.

theorem IsQuotientCoveringMap.singularCohomologyBockstein_comp_singularCohomologyIsoGroupCohomology_hom {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {S : CategoryTheory.ShortComplex (ModuleCat k)} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyBockstein (↧k) k B hS n m h) (hG.singularCohomologyIsoGroupCohomology k (↑S.X₁) m).hom = CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k (↑S.X₃) n).hom (groupCohomology.δ ⋯ n m h)

The comparison of singular cohomology with group cohomology respects the coefficient long exact sequences: for the quotient covering map p : E ⟶ B of an action of G with contractible total space and a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of k-modules, the isomorphisms Hⁿ(B; Mᵢ) ≅ Hⁿ(G, Mᵢ) carry the Bockstein homomorphism Hⁿ(B; M₃) ⟶ Hᵐ(B; M₁), n + 1 = m, to Mathlib's connecting map groupCohomology.δ of the short exact sequence of trivial representations.

theorem IsQuotientCoveringMap.singularCohomologyBockstein_comp_singularCohomologyIsoGroupCohomology_hom_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {S : CategoryTheory.ShortComplex (ModuleCat k)} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : groupCohomology (Rep.trivial k G ↑S.X₁) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyBockstein (↧k) k B hS n m h) (CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k (↑S.X₁) m).hom h✝) = CategoryTheory.CategoryStruct.comp (hG.singularCohomologyIsoGroupCohomology k (↑S.X₃) n).hom (CategoryTheory.CategoryStruct.comp (groupCohomology.δ ⋯ n m h) h✝)

The comparison of singular cohomology with group cohomology respects the coefficient long exact sequences: for the quotient covering map p : E ⟶ B of an action of G with contractible total space and a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of k-modules, the isomorphisms Hⁿ(B; Mᵢ) ≅ Hⁿ(G, Mᵢ) carry the Bockstein homomorphism Hⁿ(B; M₃) ⟶ Hᵐ(B; M₁), n + 1 = m, to Mathlib's connecting map groupCohomology.δ of the short exact sequence of trivial representations.