The coefficient long exact sequence and the Bockstein homomorphism

Let 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 be a short exact sequence of coefficients in a k-linear abelian category C with coproducts, and let R : C be projective; for the usual singular cohomology with coefficients in k-modules, take C := ModuleCat k and R := k. The singular chains Cₙ(X; R) of a space are a coproduct of copies of R, hence projective (SSet.projective_chainComplex_X_of_projective), and so are the relative chains Cₙ(X, A; R) of a pair, which are a direct summand of Cₙ(X; R). The functors Hom(C(X; R), -) and Hom(C(X, A; R), -) of the coefficients are therefore exact, which gives short exact sequences of singular cochain complexes

0 ⟶ C*(X; M₁) ⟶ C*(X; M₂) ⟶ C*(X; M₃) ⟶ 0, 0 ⟶ C*(X, A; M₁) ⟶ C*(X, A; M₂) ⟶ C*(X, A; M₃) ⟶ 0.

Their connecting morphisms are the Bockstein homomorphisms Hⁿ(X; M₃) ⟶ Hⁿ⁺¹(X; M₁) and Hⁿ(X, A; M₃) ⟶ Hⁿ⁺¹(X, A; M₁), and their long exact cohomology sequences are the coefficient long exact sequences

⋯ ⟶ Hⁿ(X; M₁) ⟶ Hⁿ(X; M₂) ⟶ Hⁿ(X; M₃) ⟶ Hⁿ⁺¹(X; M₁) ⟶ ⋯,

whose maps between the cohomology groups with the same degree are induced by the coefficient maps. The Bockstein homomorphism is natural in continuous maps, respectively maps of pairs, and in morphisms of short exact sequences of coefficients.

Exactness in the coefficients is the only input: for a fixed chain complex K whose terms are projective, Hom(K, -) is exact (ChainComplex.shortExact_map_linearYonedaObjFunctor). It is not the long exact sequence of a pair, which instead uses that the chain sequence of a pair splits in each degree.

Main declarations

• TopCat.singularCochainComplexCoefficientShortComplex and TopCat.shortExact_singularCochainComplexCoefficientShortComplex: the short exact sequence of singular cochain complexes induced by a short exact sequence of coefficients.
• TopCat.singularCohomologyBockstein: the Bockstein homomorphism Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁) for n + 1 = m, with the three exactness statements TopCat.singularCohomology_exact_coefficient₁, TopCat.singularCohomology_exact_coefficient₂ and TopCat.singularCohomology_exact_coefficient₃ and the naturality statements TopCat.singularCohomologyBockstein_naturality and TopCat.singularCohomologyBockstein_naturality_coefficients.
• TopPair.singularCochainComplexCoefficientShortComplex, TopPair.singularCohomologyBockstein and their exactness and naturality statements: the same for relative singular cohomology.

References

• A. Hatcher, Algebraic Topology, Section 3.E.

@[reducible, inline]

noncomputable abbrev TopCat.singularCochainComplexCoefficientShortComplex {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] (X : TopCat) (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The sequence of singular cochain complexes C*(X; S.X₁) ⟶ C*(X; S.X₂) ⟶ C*(X; S.X₃) induced by a short complex S of coefficients: its maps are postcomposition with the maps of S.

noncomputable def TopCat.singularCochainComplexCoefficientShortComplexMap {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] {X Y : TopCat} (f : X ⟶ Y) (S : CategoryTheory.ShortComplex C) : singularCochainComplexCoefficientShortComplex R k Y S ⟶ singularCochainComplexCoefficientShortComplex R k X S

The morphism from the coefficient cochain sequence of Y to that of X induced by a continuous map f : X ⟶ Y: its components are the cochain maps induced by f.

@[simp]

theorem TopCat.singularCochainComplexCoefficientShortComplexMap_τ₁ {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] {X Y : TopCat} (f : X ⟶ Y) (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₁ = singularCochainComplexMap f

@[simp]

theorem TopCat.singularCochainComplexCoefficientShortComplexMap_τ₂ {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] {X Y : TopCat} (f : X ⟶ Y) (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₂ = singularCochainComplexMap f

@[simp]

theorem TopCat.singularCochainComplexCoefficientShortComplexMap_τ₃ {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] {X Y : TopCat} (f : X ⟶ Y) (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₃ = singularCochainComplexMap f

theorem TopCat.shortExact_singularCochainComplexCoefficientShortComplex {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : (singularCochainComplexCoefficientShortComplex R k X S).ShortExact

A short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of coefficients induces a short exact sequence 0 ⟶ C*(X; M₁) ⟶ C*(X; M₂) ⟶ C*(X; M₃) ⟶ 0 of singular cochain complexes.

noncomputable def TopCat.singularCohomologyBockstein {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : TopCat.singularCohomology R k S.X₃ X n ⟶ TopCat.singularCohomology R k S.X₁ X m

The Bockstein homomorphism Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁), for n + 1 = m, of a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of coefficients: the connecting morphism of the long exact cohomology sequence of the short exact sequence of singular cochain complexes.

theorem TopCat.singularCohomologyBockstein_eq_δ {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : singularCohomologyBockstein R k X hS n m h = ⋯.δ n m ⋯

The Bockstein homomorphism is, by definition, the connecting morphism of the short exact sequence 0 ⟶ C*(X; M₁) ⟶ C*(X; M₂) ⟶ C*(X; M₃) ⟶ 0 of singular cochain complexes.

@[simp]

theorem TopCat.comp_singularCohomologyBockstein {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.g) n) (singularCohomologyBockstein R k X hS n m h) = 0

@[simp]

theorem TopCat.comp_singularCohomologyBockstein_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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : TopCat.singularCohomology R k S.X₁ X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.g) n) (CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.singularCohomologyBockstein_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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.f) m) = 0

@[simp]

theorem TopCat.singularCohomologyBockstein_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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology (((toSSet.obj X).chainComplex R).linearYonedaObj k S.X₂) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.f) m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.singularCohomology_exact_coefficient₁ {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := TopCat.singularCohomology R k S.X₃ X n, X₂ := TopCat.singularCohomology R k S.X₁ X m, X₃ := HomologicalComplex.homology (((toSSet.obj X).chainComplex R).linearYonedaObj k S.X₂) m, f := singularCohomologyBockstein R k X hS n m h, g := HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.f) m, zero := ⋯ }.Exact

Exactness at Hᵐ(X; M₁): Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁) ⟶ Hᵐ(X; M₂) is exact for n + 1 = m.

theorem TopCat.singularCohomology_exact_coefficient₂ {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n : ℕ) : ((singularCochainComplexCoefficientShortComplex R k X S).map (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.up ℕ) n)).Exact

Exactness at Hⁿ(X; M₂): Hⁿ(X; M₁) ⟶ Hⁿ(X; M₂) ⟶ Hⁿ(X; M₃) is exact.

theorem TopCat.singularCohomology_exact_coefficient₃ {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] [CategoryTheory.Projective R] (X : TopCat) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology (((toSSet.obj X).chainComplex R).linearYonedaObj k S.X₂) n, X₂ := HomologicalComplex.homology (((toSSet.obj X).chainComplex R).linearYonedaObj k S.X₃) n, X₃ := TopCat.singularCohomology R k S.X₁ X m, f := HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) S.g) n, g := singularCohomologyBockstein R k X hS n m h, zero := ⋯ }.Exact

Exactness at Hⁿ(X; M₃): Hⁿ(X; M₂) ⟶ Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁) is exact for n + 1 = m.

theorem TopCat.singularCohomologyBockstein_naturality {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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X Y : TopCat} (f : X ⟶ Y) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k Y hS n m h) (TopCat.singularCohomologyMap f m) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f n) (singularCohomologyBockstein R k X hS n m h)

The Bockstein homomorphism is natural in the space: for a continuous map f : X ⟶ Y, following Hⁿ(Y; M₃) ⟶ Hᵐ(Y; M₁) by the map induced by f agrees with following the map induced by f by Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁).

theorem TopCat.singularCohomologyBockstein_naturality_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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X Y : TopCat} (f : X ⟶ Y) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : TopCat.singularCohomology R k S.X₁ X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k Y hS n m h) (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f m) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f n) (CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) h✝)

The Bockstein homomorphism is natural in the space: for a continuous map f : X ⟶ Y, following Hⁿ(Y; M₃) ⟶ Hᵐ(Y; M₁) by the map induced by f agrees with following the map induced by f by Hⁿ(X; M₃) ⟶ Hᵐ(X; M₁).

theorem TopCat.singularCohomologyBockstein_naturality_coefficients {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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (X : TopCat) {S' : CategoryTheory.ShortComplex C} (hS' : S'.ShortExact) (φ : S ⟶ S') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) φ.τ₁) m) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) φ.τ₃) n) (singularCohomologyBockstein R k X hS' n m h)

The Bockstein homomorphism is natural in the short exact sequence of coefficients: a morphism φ : S ⟶ S' of short exact sequences of coefficients commutes with the Bockstein homomorphisms of S and S' and the maps on singular cohomology induced by its components.

theorem TopCat.singularCohomologyBockstein_naturality_coefficients_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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (X : TopCat) {S' : CategoryTheory.ShortComplex C} (hS' : S'.ShortExact) (φ : S ⟶ S') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology (((toSSet.obj X).chainComplex R).linearYonedaObj k S'.X₁) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) φ.τ₁) m) h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((toSSet.obj X).chainComplex R) φ.τ₃) n) (CategoryTheory.CategoryStruct.comp (singularCohomologyBockstein R k X hS' n m h) h✝)

The Bockstein homomorphism is natural in the short exact sequence of coefficients: a morphism φ : S ⟶ S' of short exact sequences of coefficients commutes with the Bockstein homomorphisms of S and S' and the maps on singular cohomology induced by its components.

@[reducible, inline]

noncomputable abbrev TopPair.singularCochainComplexCoefficientShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The sequence of relative singular cochain complexes C*(X, A; S.X₁) ⟶ C*(X, A; S.X₂) ⟶ C*(X, A; S.X₃) of a pair (X, A) induced by a short complex S of coefficients: its maps are postcomposition with the maps of S.

noncomputable def TopPair.singularCochainComplexCoefficientShortComplexMap {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] {P P' : TopPair} (f : P ⟶ P') (S : CategoryTheory.ShortComplex C) : P'.singularCochainComplexCoefficientShortComplex R k S ⟶ P.singularCochainComplexCoefficientShortComplex R k S

The morphism from the coefficient cochain sequence of (Y, B) to that of (X, A) induced by a map of pairs f : (X, A) ⟶ (Y, B): its components are the relative cochain maps induced by f.

@[simp]

theorem TopPair.singularCochainComplexCoefficientShortComplexMap_τ₁ {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] {P P' : TopPair} (f : P ⟶ P') (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₁ = singularCochainComplexMap f

@[simp]

theorem TopPair.singularCochainComplexCoefficientShortComplexMap_τ₂ {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] {P P' : TopPair} (f : P ⟶ P') (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₂ = singularCochainComplexMap f

@[simp]

theorem TopPair.singularCochainComplexCoefficientShortComplexMap_τ₃ {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] {P P' : TopPair} (f : P ⟶ P') (S : CategoryTheory.ShortComplex C) : (singularCochainComplexCoefficientShortComplexMap f S).τ₃ = singularCochainComplexMap f

theorem TopPair.shortExact_singularCochainComplexCoefficientShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : (P.singularCochainComplexCoefficientShortComplex R k S).ShortExact

A short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of coefficients induces a short exact sequence 0 ⟶ C*(X, A; M₁) ⟶ C*(X, A; M₂) ⟶ C*(X, A; M₃) ⟶ 0 of relative singular cochain complexes.

noncomputable def TopPair.singularCohomologyBockstein {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : P.singularCohomology R k S.X₃ n ⟶ P.singularCohomology R k S.X₁ m

The Bockstein homomorphism Hⁿ(X, A; M₃) ⟶ Hᵐ(X, A; M₁), for n + 1 = m, of a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of coefficients: the connecting morphism of the long exact cohomology sequence of the short exact sequence of relative singular cochain complexes.

@[simp]

theorem TopPair.comp_singularCohomologyBockstein {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.g) n) (P.singularCohomologyBockstein R k hS n m h) = 0

@[simp]

theorem TopPair.comp_singularCohomologyBockstein_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.singularCohomology R k S.X₁ m ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.g) n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopPair.singularCohomologyBockstein_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.f) m) = 0

@[simp]

theorem TopPair.singularCohomologyBockstein_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((P.singularChainComplex R).linearYonedaObj k S.X₂) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.f) m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopPair.singularCohomology_exact_coefficient₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := P.singularCohomology R k S.X₃ n, X₂ := P.singularCohomology R k S.X₁ m, X₃ := HomologicalComplex.homology ((P.singularChainComplex R).linearYonedaObj k S.X₂) m, f := P.singularCohomologyBockstein R k hS n m h, g := HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.f) m, zero := ⋯ }.Exact

Exactness at Hᵐ(X, A; M₁): Hⁿ(X, A; M₃) ⟶ Hᵐ(X, A; M₁) ⟶ Hᵐ(X, A; M₂) is exact for n + 1 = m.

theorem TopPair.singularCohomology_exact_coefficient₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n : ℕ) : ((P.singularCochainComplexCoefficientShortComplex R k S).map (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.up ℕ) n)).Exact

Exactness at Hⁿ(X, A; M₂): Hⁿ(X, A; M₁) ⟶ Hⁿ(X, A; M₂) ⟶ Hⁿ(X, A; M₃) is exact.

theorem TopPair.singularCohomology_exact_coefficient₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology ((P.singularChainComplex R).linearYonedaObj k S.X₂) n, X₂ := HomologicalComplex.homology ((P.singularChainComplex R).linearYonedaObj k S.X₃) n, X₃ := P.singularCohomology R k S.X₁ m, f := HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) S.g) n, g := P.singularCohomologyBockstein R k hS n m h, zero := ⋯ }.Exact

Exactness at Hⁿ(X, A; M₃): Hⁿ(X, A; M₂) ⟶ Hⁿ(X, A; M₃) ⟶ Hᵐ(X, A; M₁) is exact for n + 1 = m.

theorem TopPair.singularCohomologyBockstein_naturality {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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyBockstein R k hS n m h) (TopPair.singularCohomologyMap f m) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f n) (P.singularCohomologyBockstein R k hS n m h)

The relative Bockstein homomorphism is natural in maps of pairs: for f : (X, A) ⟶ (Y, B), following Hⁿ(Y, B; M₃) ⟶ Hᵐ(Y, B; M₁) by the map induced by f agrees with following the map induced by f by Hⁿ(X, A; M₃) ⟶ Hᵐ(X, A; M₁).

theorem TopPair.singularCohomologyBockstein_naturality_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] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.singularCohomology R k S.X₁ m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyBockstein R k hS n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f m) h✝) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) h✝)

The relative Bockstein homomorphism is natural in maps of pairs: for f : (X, A) ⟶ (Y, B), following Hⁿ(Y, B; M₃) ⟶ Hᵐ(Y, B; M₁) by the map induced by f agrees with following the map induced by f by Hⁿ(X, A; M₃) ⟶ Hᵐ(X, A; M₁).

theorem TopPair.singularCohomologyBockstein_naturality_coefficients {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {S' : CategoryTheory.ShortComplex C} (hS' : S'.ShortExact) (φ : S ⟶ S') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) φ.τ₁) m) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) φ.τ₃) n) (P.singularCohomologyBockstein R k hS' n m h)

The relative Bockstein homomorphism is natural in the short exact sequence of coefficients: a morphism φ : S ⟶ S' of short exact sequences of coefficients commutes with the Bockstein homomorphisms of S and S' and the maps on relative singular cohomology induced by its components.

theorem TopPair.singularCohomologyBockstein_naturality_coefficients_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Projective R] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {S' : CategoryTheory.ShortComplex C} (hS' : S'.ShortExact) (φ : S ⟶ S') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((P.singularChainComplex R).linearYonedaObj k S'.X₁) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) φ.τ₁) m) h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k (P.singularChainComplex R) φ.τ₃) n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyBockstein R k hS' n m h) h✝)

The relative Bockstein homomorphism is natural in the short exact sequence of coefficients: a morphism φ : S ⟶ S' of short exact sequences of coefficients commutes with the Bockstein homomorphisms of S and S' and the maps on relative singular cohomology induced by its components.