Documentation

TauCeti.AlgebraicTopology.Cellular.Comparison

Cellular and singular homology of finite-dimensional CW pairs #

The inclusions (Xᵐ, A) ⟶ (Xᵐ⁺¹, A) induce isomorphisms in degree k < m: the two adjacent homology groups of (Xᵐ⁺¹, Xᵐ) vanish. Hence all inclusions of skeleta above degree k induce isomorphisms in that degree. For a finite-dimensional relative CW complex, a sufficiently large skeleton is the whole complex, so the inclusion (Xᵏ⁺¹, A) ⟶ (X, A) induces an isomorphism in degree k.

Composing this inclusion-induced isomorphism with TauCeti.cellularHomologyIso identifies cellular homology with relative singular homology. The formula on cellular cycles specifies the comparison using the inclusion of pairs, without choosing singular-chain representatives. Finite dimensionality bounds cell dimensions; no finiteness of the set of cells is required. Coefficients lie in any abelian category with coproducts exact for the cell indexing types.

The source is A. Hatcher, Algebraic Topology, Section 2.2, Lemma 2.34 and Theorem 2.35.

source
theorem TauCeti.isIso_singularHomologyMap_skeletonBasePairToSucc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {m k : ℕ} [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C (m + 1))) A] (hk : k < m) :
CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToSucc C m) R k)

Attaching cells of dimension m + 1 leaves homology in degree k < m unchanged.

source
theorem TauCeti.isIso_singularHomologyMap_skeletonBasePairInclusion {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {n m k : ℕ} (h : n ≤ m) (hk : k < n) (hExact : ∀ (j : ℕ), n < j → j ≤ m → CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C j)) A) :
CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairInclusion C h) R k)

Homology in degree k is stable under inclusions of skeleta of dimension greater than k. The isomorphism is induced by the actual inclusion of pairs. Exactness of coproducts is needed only for cell dimensions n < j ≤ m.

source
theorem TauCeti.isIso_singularHomologyMap_skeletonBasePairToComplex {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [Topology.RelCWComplex.FiniteDimensional C] {m k : ℕ} (hk : k < m) (hExact : ∀ (j : ℕ), m < j → CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C j)) A) :
CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C m) R k)

For a finite-dimensional relative CW complex, inclusion of any skeleton of dimension greater than k induces an isomorphism on degree-k relative singular homology. Exactness of coproducts is needed only for cell dimensions above m.

source
noncomputable def TauCeti.cellularSingularHomologyIso {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [Topology.RelCWComplex.FiniteDimensional C] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) :
HomologicalComplex.homology (cellularChainComplex C R) n ≅ (complexBasePair C).singularHomology R n

Cellular homology of a finite-dimensional relative CW complex is its relative singular homology. The second map is induced by inclusion of the (n + 1)-skeleton into the complex.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.homologyπ_comp_cellularSingularHomologyIso_hom {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [Topology.RelCWComplex.FiniteDimensional C] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (cellularChainComplex C R) n) (cellularSingularHomologyIso C R n).hom = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (TopPair.singularHomologyMap (skeletonBasePairToComplex C n) R n)

    The cellular–singular comparison on cycles is the homology map induced by inclusion of the n-skeleton into the whole pair.

    source
    @[simp]
    theorem TauCeti.homologyπ_comp_cellularSingularHomologyIso_hom_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [Topology.RelCWComplex.FiniteDimensional C] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) {Z : A} (h : (complexBasePair C).singularHomology R n ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (cellularChainComplex C R) n) (CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C R n).hom h) = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToComplex C n) R n) h)

    The cellular–singular comparison on cycles is the homology map induced by inclusion of the n-skeleton into the whole pair.