The comparison of cubical and simplicial singular chains

The normalized cubical chains and the simplicial singular chains of a topological space are naturally chain homotopy equivalent (TauCeti.cubicalSingularHomotopyEquiv). Both comparison maps and both homotopies come from the method of acyclic models (TauCeti.Algebra.Homology.AcyclicModels): each functor is free on models, the topological simplices for the simplicial chains and the cubes for the cubical ones, and each is acyclic on every contractible space (TauCeti.AlgebraicTopology.Singular.Cubical.Comparison.Models). In degree zero the comparison maps send a point to the same point, so they are compatible with the augmentations.

This is the comparison through which the consequences of the simplicial theory (homotopy invariance, the long exact sequence of a pair, excision) are transported to cubical chains.

Main definitions

• TauCeti.singularToCubical k: the natural chain map from simplicial to normalized cubical singular chains.
• TauCeti.cubicalToSingular k: the natural chain map back.
• TauCeti.cubicalSingularHomotopyEquiv k X: the chain homotopy equivalence they form.
• TauCeti.cubicalToSingularGen k n, TauCeti.singularToCubicalGen k n: the images of the identity cube of the model Iⁿ and of the identity simplex of the model Δⁿ under the comparison maps.
• TauCeti.singularCubicalHomologyIso k X n, TauCeti.singularCubicalHomologyNatIso k n: cubical singular homology is naturally isomorphic to singular homology.
• TauCeti.cubicalCycleOfPoint k x: the point cube at x, as a cubical cycle of degree zero.

Main results

• TauCeti.singularToCubical_app_f_simplexChain and TauCeti.cubicalToSingular_app_f_ofCube: the comparison maps send a simplex, respectively a cube, to the image of the model generator under it, regarded as a map from the model.
• TauCeti.singularToCubicalCompHomotopy_hom_simplexChain and TauCeti.cubicalToSingularCompHomotopy_hom_ofCube: the natural homotopies, on a simplex or a cube, are the images of their values on the model generators.
• TauCeti.cubicalAugment_singularToCubical and TauCeti.singularAugment_cubicalToSingular: the comparison maps are compatible with the augmentations.
• TauCeti.singularToCubical_app_f_zero_simplexChain and TauCeti.cubicalToSingular_app_f_zero_ofCube: in degree zero the comparison maps send a point to the same point.
• TauCeti.cubicalToSingularGen_zero and TauCeti.singularToCubicalGen_zero: in degree zero the model generators are the point simplex and the point cube.
• TauCeti.singularCubicalHomologyIso_hom_singularHomology₀Section: on homology in degree zero the comparison sends the class of a point to the class of the point cube.
• TauCeti.TopCat.isIso_singularHomologyMap_of_quasiIso: a map inducing a quasi-isomorphism of normalized cubical chains induces isomorphisms on singular homology.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII.
• S. Eilenberg and S. Mac Lane, Acyclic models, Amer. J. Math. 75 (1953).

The comparison maps

noncomputable def TauCeti.cubicalToSingular (k : Type u) [Ring k] : normalizedCubicalChainComplex k ⟶ singularChains k

The comparison map from normalized cubical to simplicial singular chains: the natural chain map sending a point to the same point, built by acyclic models.

noncomputable def TauCeti.singularToCubical (k : Type u) [Ring k] : singularChains k ⟶ normalizedCubicalChainComplex k

The comparison map from simplicial singular to normalized cubical chains: the natural chain map sending a point to the same point, built by acyclic models.

theorem TauCeti.singularAugment_cubicalToSingular {k : Type u} [Ring k] (X : TopCat) (x : ↑(((normalizedCubicalChainComplex k).obj X).X 0)) : (singularAugment k X) ((CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app X).f 0)) x) = (cubicalAugment k X) x

The comparison map to simplicial chains is compatible with the augmentations.

theorem TauCeti.cubicalAugment_singularToCubical {k : Type u} [Ring k] (X : TopCat) (x : ↑(((singularChains k).obj X).X 0)) : (cubicalAugment k X) ((CategoryTheory.ConcreteCategory.hom (((singularToCubical k).app X).f 0)) x) = (singularAugment k X) x

The comparison map to cubical chains is compatible with the augmentations.

noncomputable def TauCeti.singularToCubicalCompHomotopy (k : Type u) [Ring k] (X : TopCat) : Homotopy (CategoryTheory.CategoryStruct.comp ((singularToCubical k).app X) ((cubicalToSingular k).app X)) (CategoryTheory.CategoryStruct.id ((singularChains k).obj X))

The composite of the comparison maps on simplicial chains is homotopic to the identity.

noncomputable def TauCeti.cubicalToSingularCompHomotopy (k : Type u) [Ring k] (X : TopCat) : Homotopy (CategoryTheory.CategoryStruct.comp ((cubicalToSingular k).app X) ((singularToCubical k).app X)) (CategoryTheory.CategoryStruct.id ((normalizedCubicalChainComplex k).obj X))

The composite of the comparison maps on cubical chains is homotopic to the identity.

theorem TauCeti.singularToCubicalCompHomotopy_hom_naturality (k : Type u) [Ring k] {X Y : TopCat} (f : X ⟶ Y) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (((singularChains k).map f).f i) ((singularToCubicalCompHomotopy k Y).hom i j) = CategoryTheory.CategoryStruct.comp ((singularToCubicalCompHomotopy k X).hom i j) (((singularChains k).map f).f j)

The homotopy singularToCubicalCompHomotopy is natural.

theorem TauCeti.cubicalToSingularCompHomotopy_hom_naturality (k : Type u) [Ring k] {X Y : TopCat} (f : X ⟶ Y) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (((normalizedCubicalChainComplex k).map f).f i) ((cubicalToSingularCompHomotopy k Y).hom i j) = CategoryTheory.CategoryStruct.comp ((cubicalToSingularCompHomotopy k X).hom i j) (((normalizedCubicalChainComplex k).map f).f j)

The homotopy cubicalToSingularCompHomotopy is natural.

noncomputable def TauCeti.cubicalSingularHomotopyEquiv (k : Type u) [Ring k] (X : TopCat) : HomotopyEquiv ((singularChains k).obj X) ((normalizedCubicalChainComplex k).obj X)

Cubical and simplicial singular chains are naturally chain homotopy equivalent.

@[simp]

theorem TauCeti.cubicalSingularHomotopyEquiv_hom (k : Type u) [Ring k] (X : TopCat) : (cubicalSingularHomotopyEquiv k X).hom = (singularToCubical k).app X

@[simp]

theorem TauCeti.cubicalSingularHomotopyEquiv_inv (k : Type u) [Ring k] (X : TopCat) : (cubicalSingularHomotopyEquiv k X).inv = (cubicalToSingular k).app X

The comparison maps in degree zero

theorem TauCeti.singularToCubical_app_f_zero_simplexChain {k : Type u} [Ring k] {X : TopCat} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) : (CategoryTheory.ConcreteCategory.hom (((singularToCubical k).app X).f 0)) (simplexChain σ 1) = NormalizedCubicalChain.ofCube (↑X) k (SingularCube.point (TopCat.toSSetObj₀Equiv σ))

The comparison map to cubical chains sends a point to the point cube.

theorem TauCeti.cubicalToSingular_app_f_zero_ofCube {k : Type u} [Ring k] {X : TopCat} (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app X).f 0)) (NormalizedCubicalChain.ofCube (↑X) k (SingularCube.point x)) = simplexChain (TopCat.toSSetObj₀Equiv.symm x) 1

The comparison map to simplicial chains sends a point cube to the point.

theorem TauCeti.cubicalToSingular_app_f_zero_ofZeroCube {k : Type u} [Ring k] {X : TopCat} (c : SingularCube (↑X) 0) : (CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app X).f 0)) (NormalizedCubicalChain.ofCube (↑X) k c) = simplexChain (TopCat.toSSetObj₀Equiv.symm (c fun (i : Fin 0) => i.elim0)) 1

The comparison map to simplicial chains sends any 0-cube to the chain of its point.

theorem TauCeti.singularChains_map_cubicalToSingular {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (c : SingularCube (↑X) n) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) ((CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app X).f n)) (NormalizedCubicalChain.ofCube (↑X) k c)) = (CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app Y).f n)) (NormalizedCubicalChain.ofCube (↑Y) k ((TopCat.Hom.hom f).comp c))

The comparison with simplicial chains is natural: pushing forward the image of a cube is the image of the pushed-forward cube.

noncomputable def TauCeti.cubicalToSingularGen (k : Type u) [Ring k] (n : ℕ) : ↑(((singularChains k).obj (cubeModel n)).X n)

The image, under the comparison with simplicial chains, of the identity cube of the model Iⁿ.

noncomputable def TauCeti.cubicalToSingularSubcube (k : Type u) [Ring k] (n : ℕ) {m : ℕ} (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) : ↑(((singularChains k).obj (cubeModel n)).X m)

The image, under the comparison with simplicial chains, of the subcube upCube n ∘ ι of the model Iⁿ.

theorem TauCeti.cubicalToSingular_app_f_ofCube (k : Type u) [Ring k] {X : TopCat} {n : ℕ} (c : SingularCube (↑X) n) : (CategoryTheory.ConcreteCategory.hom (((cubicalToSingular k).app X).f n)) (NormalizedCubicalChain.ofCube (↑X) k c) = (CategoryTheory.ConcreteCategory.hom (((singularChains k).map (cubeToHom c)).f n)) (cubicalToSingularGen k n)

The comparison with simplicial chains sends a cube to the image of the model generator under the cube, regarded as a map from the model.

@[simp]

theorem TauCeti.cubicalToSingularGen_zero (k : Type u) [Ring k] : cubicalToSingularGen k 0 = simplexChain (TopCat.toSSetObj₀Equiv.symm ((upCube 0) fun (i : Fin 0) => i.elim0)) 1

In degree zero, the model generator of the comparison to simplicial chains is the 0-simplex at the unique point of the 0-cube.

theorem TauCeti.cubicalToSingularSubcube_id (k : Type u) [Ring k] (n : ℕ) : cubicalToSingularSubcube k n (ContinuousMap.id (Fin n → ↑unitInterval)) = cubicalToSingularGen k n

The image of the identity cube is the image of its subcube along the identity.

theorem TauCeti.cubicalToSingularSubcube_eq_zero (k : Type u) [Ring k] {n m : ℕ} {ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)} (h : SingularCube.IsDegenerate (ContinuousMap.comp (upCube n) ι)) : cubicalToSingularSubcube k n ι = 0

The image of a degenerate subcube of the model is zero.

theorem TauCeti.singularChains_map_cubicalToSingularSubcube (k : Type u) [Ring k] {n m p : ℕ} (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (κ : C(Fin p → ↑unitInterval, Fin m → ↑unitInterval)) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).map (cubeToHom (ContinuousMap.comp (upCube n) ι))).f p)) (cubicalToSingularSubcube k m κ) = cubicalToSingularSubcube k n (ι.comp κ)

Pushing forward the image of a subcube of the model along a map between models is the image of the pushed-forward subcube.

theorem TauCeti.singularChains_d_cubicalToSingularGen (k : Type u) [Ring k] (n : ℕ) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj (cubeModel (n + 1))).d (n + 1) n)) (cubicalToSingularGen k (n + 1)) = ∑ i : Fin (n + 1), (-1) ^ ↑i • (cubicalToSingularSubcube k (n + 1) (SingularCube.face i 0 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))) - cubicalToSingularSubcube k (n + 1) (SingularCube.face i 1 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))))

The boundary of the image of the identity cube of the model Iⁿ⁺¹ is the alternating sum of the images of its faces.

noncomputable def TauCeti.singularToCubicalGen (k : Type u) [Ring k] (n : ℕ) : ↑(((normalizedCubicalChainComplex k).obj (simplexModel n)).X n)

The image, under the comparison with cubical chains, of the identity simplex of the model Δⁿ.

theorem TauCeti.singularToCubical_app_f_simplexChain (k : Type u) [Ring k] {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (((singularToCubical k).app X).f n)) (simplexChain σ 1) = (CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).map σ.down).f n)) (singularToCubicalGen k n)

The comparison with cubical chains sends a simplex to the image of the model generator under the simplex, regarded as a map from the model.

theorem TauCeti.singularToCubicalCompHomotopy_hom_simplexChain (k : Type u) [Ring k] {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom ((singularToCubicalCompHomotopy k X).hom n (n + 1))) (simplexChain σ 1) = (CategoryTheory.ConcreteCategory.hom (((singularChains k).map σ.down).f (n + 1))) ((CategoryTheory.ConcreteCategory.hom ((singularToCubicalCompHomotopy k (simplexModel n)).hom n (n + 1))) (simplexChain (idSimplex n) 1))

The chain homotopy singularToCubicalCompHomotopy evaluated on a simplex is the image of its value on the identity simplex of the model under the simplex, regarded as a map from the model.

theorem TauCeti.cubicalToSingularCompHomotopy_hom_ofCube (k : Type u) [Ring k] {X : TopCat} {n : ℕ} (c : SingularCube (↑X) n) : (CategoryTheory.ConcreteCategory.hom ((cubicalToSingularCompHomotopy k X).hom n (n + 1))) (NormalizedCubicalChain.ofCube (↑X) k c) = (CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).map (cubeToHom c)).f (n + 1))) ((CategoryTheory.ConcreteCategory.hom ((cubicalToSingularCompHomotopy k (cubeModel n)).hom n (n + 1))) (NormalizedCubicalChain.ofCube (↑(cubeModel n)) k (upCube n)))

The chain homotopy cubicalToSingularCompHomotopy evaluated on a cube is the image of its value on the identity cube of the model under the cube, regarded as a map from the model.

@[simp]

theorem TauCeti.singularToCubicalGen_zero (k : Type u) [Ring k] : singularToCubicalGen k 0 = NormalizedCubicalChain.ofCube (↑(simplexModel 0)) k (SingularCube.point (TopCat.toSSetObj₀Equiv (idSimplex 0)))

In degree zero, the model generator of the comparison to cubical chains is the point cube at the vertex of the 0-simplex.

Quasi-isomorphisms and the homology comparison

instance TauCeti.instQuasiIsoNatModuleCatAppTopCatChainComplexSingularToCubical {k : Type u} [Ring k] (X : TopCat) : QuasiIso ((singularToCubical k).app X)

The comparison map to cubical chains is a quasi-isomorphism.

instance TauCeti.instQuasiIsoNatModuleCatAppTopCatChainComplexCubicalToSingular {k : Type u} [Ring k] (X : TopCat) : QuasiIso ((cubicalToSingular k).app X)

The comparison map to simplicial chains is a quasi-isomorphism.

noncomputable def TauCeti.singularCubicalHomologyIso (k : Type u) [Ring k] (X : TopCat) (n : ℕ) : HomologicalComplex.homology ((singularChains k).obj X) n ≅ HomologicalComplex.homology ((normalizedCubicalChainComplex k).obj X) n

Cubical singular homology is singular homology: the isomorphism induced by the comparison of cubical and simplicial chains.

@[simp]

theorem TauCeti.singularCubicalHomologyIso_hom {k : Type u} [Ring k] (X : TopCat) (n : ℕ) : (singularCubicalHomologyIso k X n).hom = HomologicalComplex.homologyMap ((singularToCubical k).app X) n

@[simp]

theorem TauCeti.singularCubicalHomologyIso_inv {k : Type u} [Ring k] (X : TopCat) (n : ℕ) : (singularCubicalHomologyIso k X n).inv = HomologicalComplex.homologyMap ((cubicalToSingular k).app X) n

noncomputable def TauCeti.cubicalCycleOfPoint (k : Type u) [Ring k] {X : TopCat} (x : ↑X) : ↑(HomologicalComplex.cycles ((normalizedCubicalChainComplex k).obj X) 0)

The point cube at x, as a cycle of degree zero of the normalized cubical chains of X.

@[simp]

theorem TauCeti.iCycles_cubicalCycleOfPoint (k : Type u) [Ring k] {X : TopCat} (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles ((normalizedCubicalChainComplex k).obj X) 0)) (cubicalCycleOfPoint k x) = (normalizedCubicalChainComplexXEquiv X 0).symm (NormalizedCubicalChain.ofCube (↑X) k (SingularCube.point x))

theorem TauCeti.singularCubicalHomologyIso_hom_singularHomology₀Section {k : Type u} [Ring k] {X : TopCat} (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (singularCubicalHomologyIso k X 0).hom) ((ModuleCat.Hom.hom (singularHomology₀Section (↧k) x)) 1) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ ((normalizedCubicalChainComplex k).obj X) 0)) (cubicalCycleOfPoint k x)

The comparison of singular with normalized cubical homology sends the class of a point x in degree zero to the class of the point cube at x.

theorem TauCeti.singularCubicalHomologyIso_hom_naturality {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((singularChains k).map f) n) (singularCubicalHomologyIso k Y n).hom = CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k X n).hom (HomologicalComplex.homologyMap ((normalizedCubicalChainComplex k).map f) n)

The comparison isomorphism on homology is natural.

theorem TauCeti.singularCubicalHomologyIso_hom_naturality_assoc {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((normalizedCubicalChainComplex k).obj Y) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((singularChains k).map f) n) (CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k Y n).hom h) = CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k X n).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((normalizedCubicalChainComplex k).map f) n) h)

The comparison isomorphism on homology is natural.

noncomputable def TauCeti.singularCubicalHomologyNatIso (k : Type u) [Ring k] (n : ℕ) : (singularChains k).comp (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.down ℕ) n) ≅ (normalizedCubicalChainComplex k).comp (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.down ℕ) n)

Cubical singular homology is naturally isomorphic to singular homology, as functors on topological spaces.

@[simp]

theorem TauCeti.singularCubicalHomologyNatIso_app {k : Type u} [Ring k] (n : ℕ) (X : TopCat) : (singularCubicalHomologyNatIso k n).app X = singularCubicalHomologyIso k X n

theorem TauCeti.TopCat.isIso_singularHomologyMap_of_quasiIso {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) [QuasiIso ((normalizedCubicalChainComplex k).map f)] (n : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).map f)

A map of spaces which induces a quasi-isomorphism of normalized cubical chains induces isomorphisms on singular homology.