The comparison of cubical and simplicial chains with local coefficients

The comparison chain maps TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap and TauCeti.LocalCoefficientSystem.twistedSingularToCubicalMap between the normalized cubical chains with coefficients in a local system L and the simplicial singular chains with coefficients in L are inverse chain homotopy equivalences. The homotopies are obtained from the natural homotopies of the comparison without coefficients (TauCeti.singularToCubicalCompHomotopy and TauCeti.cubicalToSingularCompHomotopy) in the same way as the comparison maps themselves: the component of the homotopy on a simplex, or a cube, with a coefficient is the pushforward along it, from the model, of the value of the untwisted homotopy on the model generator.

Identities between constructions of this kind reduce to the model, generator by generator. A simplex, or a cube, with a coefficient is a pushforward from a model (TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_eq_twistedPushforward), the constructions are compatible with pushforwards (TauCeti.LocalCoefficientSystem.twistedSingularToCubical_twistedPushforward, TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_pushforward, and their analogues for the homotopies), and on the model the identities are those of the untwisted homotopies.

Main definitions

• TauCeti.LocalCoefficientSystem.twistedSingularHomotopy: the components of the homotopy on simplicial chains with coefficients, and TauCeti.LocalCoefficientSystem.twistedSingularToCubicalCompHomotopy: the homotopy from the composite to ∘ from of the comparison maps on simplicial chains to the identity.
• TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy: the components of the homotopy on normalized cubical chains with coefficients, and TauCeti.LocalCoefficientSystem.twistedCubicalToSingularCompHomotopy: the homotopy from the composite from ∘ to on normalized cubical chains to the identity.
• TauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv L: the chain homotopy equivalence between the normalized cubical chain complex with coefficients in L and the simplicial chain complex with coefficients in L.

Main results

• TauCeti.LocalCoefficientSystem.twistedSingularHomotopy_twistedPushforward and TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy_pushforward: compatibility of the homotopies with pushforwards from simply connected spaces.
• The instances QuasiIso (twistedCubicalToSingularMap L) and QuasiIso (twistedSingularToCubicalMap L): both comparison maps are quasi-isomorphisms.

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).

The homotopy on simplicial chains

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularHomotopySummand {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.twistedChainComplex.X (n + 1))

The component of the homotopy on the summand of a simplex σ: the pushforward along σ of the value of the untwisted homotopy on the identity simplex of the model.

theorem TauCeti.LocalCoefficientSystem.twistedSingularHomotopySummand_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.twistedSingularHomotopySummand σ) a = ((L.twistedPushforward (simplexToHom σ) { len := n }.toTopInitialVertex (n + 1)) ((ModuleCat.Hom.hom ((singularToCubicalCompHomotopy (ULift.{v, 0} ℤ) (simplexModel n)).hom n (n + 1))) (simplexChain (idSimplex n) 1))) a

The homotopy on a summand is the pushforward of the value of the untwisted homotopy on the model generator.

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularHomotopy {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.twistedChainComplex.X n ⟶ L.twistedChainComplex.X (n + 1)

The component of the homotopy on simplicial chains with coefficients: a simplex σ with a coefficient goes to the pushforward along σ of the value of the untwisted homotopy on the identity simplex of the model.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_comp_twistedSingularHomotopy {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.twistedSingularHomotopy n) = ModuleCat.ofHom (L.twistedSingularHomotopySummand σ)

The homotopy on the summand of a simplex.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_comp_twistedSingularHomotopy_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.twistedChainComplex.X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex n σ) (CategoryTheory.CategoryStruct.comp (L.twistedSingularHomotopy n) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (L.twistedSingularHomotopySummand σ)) h

The homotopy on the summand of a simplex.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedSingularHomotopy_ι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.twistedSingularHomotopy n)) ((CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex n σ)) a) = (L.twistedSingularHomotopySummand σ) a

The homotopy on a simplex with a coefficient.

theorem TauCeti.LocalCoefficientSystem.twistedSingularHomotopy_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₀ })) : (ModuleCat.Hom.hom (L.twistedSingularHomotopy n)) (((L.twistedPushforward f z₀ n) y) a) = ((L.twistedPushforward f z₀ (n + 1)) ((ModuleCat.Hom.hom ((singularToCubicalCompHomotopy (ULift.{v, 0} ℤ) Z).hom n (n + 1))) y)) a

Compatibility with pushforwards. The homotopy carries the simplicial pushforward of a chain of a simply connected space to the pushforward of its image under the untwisted homotopy.

theorem TauCeti.LocalCoefficientSystem.twistedSingularHomotopy_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.twistedSingularHomotopy m)) (L.simplexPushforward σ m y a) = L.simplexPushforward σ (m + 1) ((ModuleCat.Hom.hom ((singularToCubicalCompHomotopy (ULift.{v, 0} ℤ) (simplexModel n)).hom m (m + 1))) y) a

The homotopy carries the simplicial pushforward along a simplex to the pushforward of the image under the untwisted homotopy.

noncomputable def TauCeti.LocalCoefficientSystem.twistedSingularToCubicalCompHomotopy {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : Homotopy (CategoryTheory.CategoryStruct.comp L.twistedSingularToCubicalMap L.twistedCubicalToSingularMap) (CategoryTheory.CategoryStruct.id L.twistedChainComplex)

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedSingularToCubicalCompHomotopy_hom {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.twistedSingularToCubicalCompHomotopy.hom n (n + 1) = L.twistedSingularHomotopy n

The components of the homotopy twistedSingularToCubicalCompHomotopy are the maps twistedSingularHomotopy.

The homotopy on cubical chains

noncomputable def TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.NormalizedTwistedCubicalChain n →ₗ[R] L.NormalizedTwistedCubicalChain (n + 1)

The component of the homotopy on normalized cubical chains with coefficients: a cube c with a coefficient goes to the pushforward along c of the value of the untwisted homotopy on the identity cube of the model.

@[simp]

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy_ofCube {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (L.normalizedTwistedCubicalHomotopy n) ((NormalizedTwistedCubicalChain.ofCube L c) a) = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom (cubeToHom c)) (cubeModelOrigin n) (n + 1)) ((ModuleCat.Hom.hom ((cubicalToSingularCompHomotopy (ULift.{v, 0} ℤ) (cubeModel n)).hom n (n + 1))) (NormalizedCubicalChain.ofCube (↑(cubeModel n)) (ULift.{v, 0} ℤ) (upCube n)))) a

The homotopy on a cube with a coefficient: the pushforward along the cube of the value of the untwisted homotopy on the identity cube of the model.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy_pushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {Z : TopCat} [SimplyConnectedSpace ↑Z] (f : Z ⟶ X) (z₀ : ↑Z) {n : ℕ} (y : NormalizedCubicalChain (↑Z) (ULift.{v, 0} ℤ) n) (a : ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : (L.normalizedTwistedCubicalHomotopy n) (((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom f) z₀ n) y) a) = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom f) z₀ (n + 1)) ((ModuleCat.Hom.hom ((cubicalToSingularCompHomotopy (ULift.{v, 0} ℤ) Z).hom n (n + 1))) y)) a

Compatibility with pushforwards. The homotopy carries the cubical pushforward of a chain of a simply connected space to the pushforward of its image under the untwisted homotopy.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalHomotopy_cubeCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (c : SingularCube (↑X) n) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : (L.normalizedTwistedCubicalHomotopy m) (L.cubeCubicalPushforward c m y a) = L.cubeCubicalPushforward c (m + 1) ((ModuleCat.Hom.hom ((cubicalToSingularCompHomotopy (ULift.{v, 0} ℤ) (cubeModel n)).hom m (m + 1))) y) a

The homotopy on cubical chains carries the cubical pushforward along a cube to the pushforward of the image under the untwisted homotopy.

noncomputable def TauCeti.LocalCoefficientSystem.twistedCubicalToSingularCompHomotopy {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : Homotopy (CategoryTheory.CategoryStruct.comp L.twistedCubicalToSingularMap L.twistedSingularToCubicalMap) (CategoryTheory.CategoryStruct.id L.normalizedTwistedCubicalChainComplex)

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubicalToSingularCompHomotopy_hom {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.twistedCubicalToSingularCompHomotopy.hom n (n + 1) = ModuleCat.ofHom (L.normalizedTwistedCubicalHomotopy n)

The components of the homotopy twistedCubicalToSingularCompHomotopy are the maps normalizedTwistedCubicalHomotopy.

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

Cubical and simplicial chains with local coefficients are chain homotopy equivalent.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv_hom {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : L.twistedCubicalSingularHomotopyEquiv.hom = L.twistedCubicalToSingularMap

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv_inv {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : L.twistedCubicalSingularHomotopyEquiv.inv = L.twistedSingularToCubicalMap

instance TauCeti.LocalCoefficientSystem.instQuasiIsoNatModuleCatTwistedCubicalToSingularMap {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : QuasiIso L.twistedCubicalToSingularMap

The comparison map from cubical to simplicial chains with local coefficients is a quasi-isomorphism.

instance TauCeti.LocalCoefficientSystem.instQuasiIsoNatModuleCatTwistedSingularToCubicalMap {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : QuasiIso L.twistedSingularToCubicalMap

The comparison map from simplicial to cubical chains with local coefficients is a quasi-isomorphism.