Singular homology of a sublevel pair covering the whole space

Let f : X → β be any function to a preorder. If a < f ≤ b everywhere, the sublevel pair TauCeti.sublevelPair f : ({f ≤ b}, {f ≤ a}) is (X, ∅), so its relative singular homology is the singular homology of X (TauCeti.singularHomologyIsoSublevelPair). No continuity or regularity of f is needed. Since the subspace is empty, the comparison is the quotient map TopPair.singularHomologyπ, an isomorphism by TauCeti.AlgebraicTopology.Singular.Empty.

noncomputable def TauCeti.singularHomologyIsoSublevelPair {X : Type u} [TopologicalSpace X] {β : Type u_1} [Preorder β] {f : X → β} {a b : β} {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (hab : a ≤ b) (ha : ∀ (x : X), a < f x) (hb : ∀ (x : X), f x ≤ b) (R : C) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj ↧X ≅ (sublevelPair f hab).singularHomology R n

The sublevel pair of a band covering X. If a < f ≤ b everywhere, the relative singular homology of ({f ≤ b}, {f ≤ a}) = (X, ∅) is the singular homology of X. The isomorphism is the map induced by the homeomorphism X ≃ {f ≤ b}, followed by the quotient map TopPair.singularHomologyπ (TauCeti.singularHomologyπ_comp_singularHomologyIsoSublevelPair_inv).

theorem TauCeti.singularHomologyπ_comp_singularHomologyIsoSublevelPair_inv {X : Type u} [TopologicalSpace X] {β : Type u_1} [Preorder β] {f : X → β} {a b : β} {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (hab : a ≤ b) (ha : ∀ (x : X), a < f x) (hb : ∀ (x : X), f x ≤ b) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((sublevelPair f hab).singularHomologyπ R n) (singularHomologyIsoSublevelPair hab ha hb R n).inv = ((AlgebraicTopology.singularHomologyFunctor C n).obj R).map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })

The inverse of TauCeti.singularHomologyIsoSublevelPair, after the quotient map from the homology of {f ≤ b}, is the map induced by the inclusion {f ≤ b} → X.

theorem TauCeti.singularHomologyπ_comp_singularHomologyIsoSublevelPair_inv_assoc {X : Type u} [TopologicalSpace X] {β : Type u_1} [Preorder β] {f : X → β} {a b : β} {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (hab : a ≤ b) (ha : ∀ (x : X), a < f x) (hb : ∀ (x : X), f x ≤ b) (R : C) (n : ℕ) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj ↧X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((sublevelPair f hab).singularHomologyπ R n) (CategoryTheory.CategoryStruct.comp (singularHomologyIsoSublevelPair hab ha hb R n).inv h) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C n).obj R).map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })) h

The inverse of TauCeti.singularHomologyIsoSublevelPair, after the quotient map from the homology of {f ≤ b}, is the map induced by the inclusion {f ≤ b} → X.