The models of the cubical–simplicial comparison

The simplicial singular chains are free on the topological simplices Δⁿ, with generator the identity simplex, and the normalized cubical chains are free on the cubes Iⁿ in the sense of TauCeti.AcyclicModels.ModelPresentation, through the normalization of TauCeti.AlgebraicTopology.Singular.Cubical.Normalization. Both are acyclic on every contractible space, in particular on both kinds of models: the cubical chains by the cone of TauCeti.AlgebraicTopology.Singular.Cubical.Cone, the simplicial chains by the vanishing of the singular homology of a contractible space and the computation of H₀ of a connected simplicial set.

Main definitions

• TauCeti.singularModelPresentation k, TauCeti.cubicalModelPresentation k: the two functors are free on models.

Main results

• TauCeti.isAcyclicOn_singularChains, TauCeti.isAcyclicOn_normalizedCubicalChainComplex: both functors are acyclic on families of contractible spaces.

Singular simplices

@[simp]

theorem TauCeti.toSSet_map_app_down {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) σ).down = CategoryTheory.CategoryStruct.comp σ.down f

The underlying morphism of a pushed-forward singular simplex.

noncomputable def TauCeti.singularCoord (k : Type u) [Ring k] (X : TopCat) (n : ℕ) : ↑(((singularChains k).obj X).X n) →ₗ[k] (simplexModel n ⟶ X) →₀ k

The coefficients of a simplicial singular chain on the maps from the topological simplex.

@[simp]

theorem TauCeti.singularCoord_simplexChain {k : Type u} [Ring k] (X : TopCat) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : k) : (singularCoord k X n) (simplexChain σ a) = Finsupp.single σ.down a

noncomputable def TauCeti.singularModelPresentation (k : Type u) [Ring k] : AcyclicModels.ModelPresentation (singularChains k)

The simplicial singular chains are free on the topological simplices.

@[simp]

theorem TauCeti.singularModelPresentation_model (k : Type u) [Ring k] (n : ℕ) : (singularModelPresentation k).model n = simplexModel n

theorem TauCeti.singularModelPresentation_gen (k : Type u) [Ring k] (n : ℕ) : (singularModelPresentation k).gen n = simplexChain (idSimplex n) 1

theorem TauCeti.singularModelPresentation_coord (k : Type u) [Ring k] (X : TopCat) (n : ℕ) : (singularModelPresentation k).coord X n = singularCoord k X n

The cubical models

@[reducible, inline]

abbrev TauCeti.cubeModel (n : ℕ) : TopCat

The cube Iⁿ, the model of the normalized cubical chains in degree n.

def TauCeti.upCube (n : ℕ) : SingularCube (↑(cubeModel n)) n

The identity cube of the model, up to the universe lift.

@[reducible, inline]

abbrev TauCeti.cubeModelOrigin (n : ℕ) : ↑(cubeModel n)

The origin of the model Iⁿ.

def TauCeti.cubeToHom {X : TopCat} {n : ℕ} (c : SingularCube (↑X) n) : cubeModel n ⟶ X

A singular cube, as a map from the model.

@[simp]

theorem TauCeti.cubeToHom_apply {X : TopCat} {n : ℕ} (c : SingularCube (↑X) n) (x : ↑(cubeModel n)) : (CategoryTheory.ConcreteCategory.hom (cubeToHom c)) x = c x.down

@[simp]

theorem TauCeti.cubeToHom_comp {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (c : SingularCube (↑X) n) : cubeToHom ((TopCat.Hom.hom f).comp c) = CategoryTheory.CategoryStruct.comp (cubeToHom c) f

@[simp]

theorem TauCeti.cubeToHom_hom_comp_upCube {X : TopCat} {n : ℕ} (c : SingularCube (↑X) n) : (TopCat.Hom.hom (cubeToHom c)).comp (upCube n) = c

noncomputable def TauCeti.cubicalCoord (k : Type u) [Ring k] (X : TopCat) (n : ℕ) : NormalizedCubicalChain (↑X) k n →ₗ[k] (cubeModel n ⟶ X) →₀ k

The coefficients of a normalized cubical chain on the maps from the cube: the coefficients of its normalization.

theorem TauCeti.mapDomain_cubeToHom_map {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (c : CubicalChain (↑X) k n) : Finsupp.mapDomain cubeToHom ((CubicalChain.map k (TopCat.Hom.hom f) n) c) = Finsupp.mapDomain (fun (x : cubeModel n ⟶ X) => CategoryTheory.CategoryStruct.comp x f) (Finsupp.mapDomain cubeToHom c)

theorem TauCeti.cubicalCoord_map {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (x : NormalizedCubicalChain (↑X) k n) : (cubicalCoord k Y n) ((NormalizedCubicalChain.map k (TopCat.Hom.hom f) n) x) = Finsupp.mapDomain (fun (x : cubeModel n ⟶ X) => CategoryTheory.CategoryStruct.comp x f) ((cubicalCoord k X n) x)

theorem TauCeti.sum_cubicalCoord {k : Type u} [Ring k] {X : TopCat} {n : ℕ} (x : NormalizedCubicalChain (↑X) k n) : (((cubicalCoord k X n) x).sum fun (σ : cubeModel n ⟶ X) (a : k) => a • (NormalizedCubicalChain.map k (TopCat.Hom.hom σ) n) (NormalizedCubicalChain.ofCube (↑(cubeModel n)) k (upCube n))) = x

noncomputable def TauCeti.cubicalModelPresentation (k : Type u) [Ring k] : AcyclicModels.ModelPresentation (normalizedCubicalChainComplex k)

The normalized cubical chains are free on the cubes, through the normalization.

@[simp]

theorem TauCeti.cubicalModelPresentation_model (k : Type u) [Ring k] (n : ℕ) : (cubicalModelPresentation k).model n = cubeModel n

theorem TauCeti.cubicalModelPresentation_gen (k : Type u) [Ring k] (n : ℕ) : (cubicalModelPresentation k).gen n = NormalizedCubicalChain.ofCube (↑(cubeModel n)) k (upCube n)

theorem TauCeti.cubicalModelPresentation_coord (k : Type u) [Ring k] (X : TopCat) (n : ℕ) : (cubicalModelPresentation k).coord X n = cubicalCoord k X n

instance TauCeti.instContractibleSpaceCarrierCubeModel (n : ℕ) : ContractibleSpace ↑(cubeModel n)

The cube models are contractible.

Augmentations and acyclicity

@[reducible, inline]

noncomputable abbrev TauCeti.cubicalAugment (k : Type u) [Ring k] (X : TopCat) : ↑(((normalizedCubicalChainComplex k).obj X).X 0) →ₗ[k] k

The augmentation of the normalized cubical chains.

theorem TauCeti.isAcyclicOn_normalizedCubicalChainComplex {k : Type u} [Ring k] (M : ℕ → TopCat) [∀ (n : ℕ), ContractibleSpace ↑(M n)] : AcyclicModels.IsAcyclicOn (normalizedCubicalChainComplex k) M (cubicalAugment k)

The normalized cubical chains are acyclic on contractible models.

theorem TauCeti.isAcyclicOn_singularChains {k : Type u} [Ring k] (M : ℕ → TopCat) [∀ (n : ℕ), ContractibleSpace ↑(M n)] : AcyclicModels.IsAcyclicOn (singularChains k) M (singularAugment k)

The simplicial singular chains are acyclic on contractible models.

theorem TauCeti.isAcyclicOn_singularChains_cubicalModelPresentation (k : Type u) [Ring k] : AcyclicModels.IsAcyclicOn (singularChains k) (cubicalModelPresentation k).model (singularAugment k)

The simplicial singular chains are acyclic on the models of the normalized cubical chains.

theorem TauCeti.isAcyclicOn_normalizedCubicalChainComplex_singularModelPresentation (k : Type u) [Ring k] : AcyclicModels.IsAcyclicOn (normalizedCubicalChainComplex k) (singularModelPresentation k).model (cubicalAugment k)

The normalized cubical chains are acyclic on the models of the simplicial singular chains.

theorem TauCeti.isAcyclicOn_singularChains_singularModelPresentation (k : Type u) [Ring k] : AcyclicModels.IsAcyclicOn (singularChains k) (singularModelPresentation k).model (singularAugment k)

The simplicial singular chains are acyclic on their own models.

theorem TauCeti.isAcyclicOn_normalizedCubicalChainComplex_cubicalModelPresentation (k : Type u) [Ring k] : AcyclicModels.IsAcyclicOn (normalizedCubicalChainComplex k) (cubicalModelPresentation k).model (cubicalAugment k)

The normalized cubical chains are acyclic on their own models.

Properties of the cubical augmentation

theorem TauCeti.cubicalAugment_map {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) (x : ↑(((normalizedCubicalChainComplex k).obj X).X 0)) : (cubicalAugment k Y) ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).map f).f 0)) x) = (cubicalAugment k X) x

The augmentation of the normalized cubical chains is natural.

theorem TauCeti.cubicalAugment_d {k : Type u} [Ring k] (X : TopCat) (x : ↑(((normalizedCubicalChainComplex k).obj X).X 1)) : (cubicalAugment k X) ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).obj X).d 1 0)) x) = 0

The augmentation of the normalized cubical chains vanishes on boundaries.

The degree-zero data of the comparison maps

def TauCeti.cubeModelPoint : ↑(cubeModel 0)

The point of the 0-cube.

noncomputable def TauCeti.cubicalToSingularGen₀ (k : Type u) [Ring k] : ↑(((singularChains k).obj ((cubicalModelPresentation k).model 0)).X 0)

The 0-simplex at the point of the 0-cube: the value on the model of the comparison map from cubical to simplicial chains in degree zero.

noncomputable def TauCeti.singularToCubicalGen₀ (k : Type u) [Ring k] : ↑(((normalizedCubicalChainComplex k).obj ((singularModelPresentation k).model 0)).X 0)

The 0-cube at the vertex of the 0-simplex: the value on the model of the comparison map from simplicial to cubical chains in degree zero.

theorem TauCeti.cubicalToSingularGen₀_eq (k : Type u) [Ring k] : cubicalToSingularGen₀ k = simplexChain (TopCat.toSSetObj₀Equiv.symm cubeModelPoint) 1

theorem TauCeti.singularToCubicalGen₀_eq (k : Type u) [Ring k] : singularToCubicalGen₀ k = NormalizedCubicalChain.ofCube (↑(simplexModel 0)) k (SingularCube.point { len := 0 }.toTopInitialVertex)

theorem TauCeti.singularAugment_extend_cubicalToSingularGen₀ (k : Type u) [Ring k] (X : TopCat) (x : ↑(((normalizedCubicalChainComplex k).obj X).X 0)) : (singularAugment k X) (((cubicalModelPresentation k).extend (cubicalToSingularGen₀ k) X) x) = (cubicalAugment k X) x

The comparison map to simplicial chains in degree zero preserves augmentations.

theorem TauCeti.cubicalAugment_extend_singularToCubicalGen₀ (k : Type u) [Ring k] (X : TopCat) (x : ↑(((singularChains k).obj X).X 0)) : (cubicalAugment k X) (((singularModelPresentation k).extend (singularToCubicalGen₀ k) X) x) = (singularAugment k X) x

The comparison map to cubical chains in degree zero preserves augmentations.

The maps determined on the models, on generators

theorem TauCeti.singularModelPresentation_extend_simplexChain {k : Type u} [Ring k] {G : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat k) ℕ)} {m n : ℕ} (t : ↑((G.obj ((singularModelPresentation k).model n)).X m)) {X : TopCat} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : ((singularModelPresentation k).extend t X) (simplexChain σ 1) = (CategoryTheory.ConcreteCategory.hom ((G.map σ.down).f m)) t

On the chain of a simplex, the map determined by an element t on the simplicial model is the image of t under that simplex.

theorem TauCeti.cubicalModelPresentation_extend_ofCube_zero {k : Type u} [Ring k] {G : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat k) ℕ)} {m : ℕ} (t : ↑((G.obj ((cubicalModelPresentation k).model 0)).X m)) {X : TopCat} (c : SingularCube (↑X) 0) : ((cubicalModelPresentation k).extend t X) (NormalizedCubicalChain.ofCube (↑X) k c) = (CategoryTheory.ConcreteCategory.hom ((G.map (cubeToHom c)).f m)) t

On the class of a point cube, the map determined by an element t on the 0-cube is the image of t under the corresponding map from the 0-cube.