From simplicial to cubical chains with local coefficients

The comparison TauCeti.singularToCubical of the simplicial singular chains with the normalized cubical chains is natural, and the model Δⁿ is contractible, so it extends to chains with local coefficients exactly as the comparison in the other direction does (TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap). For a singular n-simplex σ of X and a coefficient a in the fibre at its initial vertex, the image is the twisted cubical pushforward (TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward) along σ, regarded as a map from the model, of the image TauCeti.singularToCubicalGen n of the identity simplex of the model, with the coefficient a at the initial vertex of the model.

The decisive property is the compatibility with pushforwards from simply connected spaces (TauCeti.LocalCoefficientSystem.twistedSingularToCubical_twistedPushforward): the comparison carries the simplicial pushforward of a chain of a simply connected space Z to the cubical pushforward of its image. Every simplex with a coefficient is such a pushforward from a standard simplex, so identities between natural maps reduce, generator by generator, to the model, where they are the untwisted ones. Here this gives the chain map property. The analogous compatibility of the comparison in the other direction is TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_pushforward.

Main definitions

• TauCeti.LocalCoefficientSystem.twistedSingularToCubical L n: the comparison on the n-chains with coefficients in L.
• TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap L: the comparison chain map from TauCeti.LocalCoefficientSystem.twistedChainComplex L to the normalized cubical chain complex with coefficients in L.

Main results

• TauCeti.LocalCoefficientSystem.twistedSingularToCubical_ιTwistedChainComplex_const: on a point simplex the comparison is the class of the point cube.
• TauCeti.LocalCoefficientSystem.twistedSingularToCubical_twistedPushforward: compatibility with pushforwards from simply connected spaces.
• TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap_naturality, TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap_coefficientMap_naturality: naturality in the space and in the local system.

References

• J.-P. Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. 54 (1951), Chapter II.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapters VII and XIV.
• S. Eilenberg and S. Mac Lane, Acyclic models, Amer. J. Math. 75 (1953).

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularToCubicalSummand {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : ↑(L.obj (initialVertex σ)) →ₗ[R] L.NormalizedTwistedCubicalChain n

The comparison from the summand of a simplex σ: the pushforward along σ, from the initial vertex of the model, of the image of the identity simplex.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubicalSummand_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : ↑(L.obj (initialVertex σ))) : (L.twistedSingularToCubicalSummand σ) a = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom (simplexToHom σ)) { len := n }.toTopInitialVertex n) (singularToCubicalGen (ULift.{v, 0} ℤ) n)) a

The comparison on the summand of a simplex is the cubical pushforward of the model generator along the simplex. This is the defining equation of twistedSingularToCubicalSummand.

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularToCubical {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.twistedChainComplex.X n ⟶ ↧(L.NormalizedTwistedCubicalChain n)

The comparison from the simplicial chains with coefficients in L to the normalized cubical chains with coefficients in L: a simplex σ with a coefficient goes to the pushforward along σ of the image of the identity simplex of the model.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_comp_twistedSingularToCubical {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex n σ) (L.twistedSingularToCubical n) = ModuleCat.ofHom (L.twistedSingularToCubicalSummand σ)

The comparison on the summand of a simplex.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_comp_twistedSingularToCubical_assoc {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) {Z : ModuleCat R} (h : ↧(L.NormalizedTwistedCubicalChain n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex n σ) (CategoryTheory.CategoryStruct.comp (L.twistedSingularToCubical n) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (L.twistedSingularToCubicalSummand σ)) h

The comparison on the summand of a simplex.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_ιTwistedChainComplex {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : ↑(L.obj (initialVertex σ))) : (ModuleCat.Hom.hom (L.twistedSingularToCubical n)) ((CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex n σ)) a) = (L.twistedSingularToCubicalSummand σ) a

The comparison on a simplex with a coefficient.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_ιTwistedChainComplex_const {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (x : ↑X) (a : ↑(L.obj { as := x })) : (ModuleCat.Hom.hom (L.twistedSingularToCubical 0)) ((CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex 0 { down := TopCat.ofHom (ContinuousMap.const (ULift.{v, 0} ↑(SimplexCategory.toTop₀.obj (Opposite.unop (Opposite.op { len := 0 })))) x) })) a) = (NormalizedTwistedCubicalChain.ofCube L (ContinuousMap.const (Fin 0 → ↑unitInterval) x)) a

On a point simplex, the comparison to cubical chains is the class of the point cube.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_twistedPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {Z : TopCat} [SimplyConnectedSpace ↑Z] (f : Z ⟶ X) (z₀ : ↑Z) {n : ℕ} (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj Z).X n)) (a : ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : (CategoryTheory.ConcreteCategory.hom (L.twistedSingularToCubical n)) (((L.twistedPushforward f z₀ n) y) a) = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom f) z₀ n) ((CategoryTheory.ConcreteCategory.hom (((singularToCubical (ULift.{v, 0} ℤ)).app Z).f n)) y)) a

Compatibility with pushforwards. The comparison carries the simplicial pushforward of a chain of a simply connected space Z to the cubical pushforward of the image of the chain.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_simplexPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex σ))) : (ModuleCat.Hom.hom (L.twistedSingularToCubical m)) (L.simplexPushforward σ m y a) = L.simplexCubicalPushforward σ m ((CategoryTheory.ConcreteCategory.hom (((singularToCubical (ULift.{v, 0} ℤ)).app (simplexModel n)).f m)) y) a

The comparison carries the simplicial pushforward along a simplex to the cubical pushforward of the image under the comparison without coefficients.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_comm {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (L.twistedChainComplex.d (n + 1) n) (L.twistedSingularToCubical n) = CategoryTheory.CategoryStruct.comp (L.twistedSingularToCubical (n + 1)) (L.normalizedTwistedCubicalChainComplex.d (n + 1) n)

The comparison from simplicial to cubical chains commutes with the boundaries.

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : L.twistedChainComplex ⟶ L.normalizedTwistedCubicalChainComplex

The comparison chain map from the simplicial chain complex with coefficients in L to the normalized cubical chain complex with coefficients in L.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap_f {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.twistedSingularToCubicalMap.f n = L.twistedSingularToCubical n

The components of the comparison chain map.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) L.twistedSingularToCubicalMap = CategoryTheory.CategoryStruct.comp ((pullback (TopCat.Hom.hom f)).obj L).twistedSingularToCubicalMap (normalizedTwistedCubicalChainComplexMap (TopCat.Hom.hom f) L)

Naturality in the space of the comparison chain map.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap_coefficientMap_naturality {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {K : LocalCoefficientSystem R X} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap η) K.twistedSingularToCubicalMap = CategoryTheory.CategoryStruct.comp L.twistedSingularToCubicalMap (normalizedTwistedCubicalChainComplexCoefficientMap η)

Naturality in the local system of the comparison chain map.

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubical_twistedCubePushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (c : SingularCube (↑X) n) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : (ModuleCat.Hom.hom (L.twistedSingularToCubical m)) (((L.twistedCubePushforward c m) y) a) = L.cubeCubicalPushforward c m ((CategoryTheory.ConcreteCategory.hom (((singularToCubical (ULift.{v, 0} ℤ)).app (cubeModel n)).f m)) y) a

The comparison to cubical chains carries the simplicial pushforward along a cube to the cubical pushforward of the image under the untwisted comparison.