From cubical to simplicial chains with local coefficients

The comparison TauCeti.cubicalToSingular of the normalized cubical chains with the simplicial singular chains is natural, and the model Iⁿ is contractible. A local system is trivialized on a contractible space, so the comparison extends to chains with local coefficients by transporting the coefficient inside the model. For a singular n-cube c of X and a coefficient a ∈ L(c 0), the image is the twisted pushforward (TauCeti.LocalCoefficientSystem.twistedPushforward) along c, regarded as a map from the model, of the image y_n of the identity cube of the model (TauCeti.cubicalToSingularGen), with the coefficient a at the origin of the model.

The key formula (TauCeti.LocalCoefficientSystem.twistedCubicalToSingular_ofSubcube) gives the image of a subcube c ∘ ι of c, with its transported coefficient, as the pushforward along c of the image of the subcube upCube ∘ ι of the model. It shows that degenerate cubes go to zero, because the comparison is defined on normalized chains, and that the boundary is respected, because the comparison is a chain map and the boundary of a cube is an alternating sum of subcubes.

The resulting chain map TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap L from the normalized cubical chain complex with coefficients in L to TauCeti.LocalCoefficientSystem.twistedChainComplex L is natural in the space and in the local system.

Main definitions

• TauCeti.cubicalToSingularGen k n: the image of the identity cube of the model under the comparison.
• TauCeti.LocalCoefficientSystem.twistedCubicalToSingular L n: the linear map from the cubical chains with coefficients in L to the simplicial ones.
• TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap L: the induced chain map on the normalized chain complex.
• TauCeti.LocalCoefficientSystem.simplexPushforward, TauCeti.LocalCoefficientSystem.simplexCubicalPushforward, TauCeti.LocalCoefficientSystem.cubeCubicalPushforward: the pushforwards along a simplex or a cube, from the model, of simplicial or cubical chains, with their additivity, boundary and differential lemmas and their compatibility with the comparison to simplicial chains.

Main results

• TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_ofCube_const: on a point cube the comparison is the inclusion of the point simplex.
• TauCeti.LocalCoefficientSystem.twistedCubicalToSingular_ofSubcube: the image of a subcube.
• TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_pushforward: compatibility with the pushforwards from simply connected spaces.
• TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap_naturality, TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap_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, Chapter XIV.

noncomputable def TauCeti.LocalCoefficientSystem.twistedCubePushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) (m : ℕ) : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m) →ₗ[ULift.{v, 0} ℤ] ↑(L.obj { as := c 0 }) →ₗ[R] ↑(L.twistedChainComplex.X m)

The pushforward along a cube: a simplicial chain of the model Iⁿ goes to the simplicial chains of X with coefficients in L by the twisted pushforward along c, regarded as a map from the model, from the origin of the model.

noncomputable def TauCeti.LocalCoefficientSystem.twistedCubicalToSingular {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : L.TwistedCubicalChain n →ₗ[R] ↑(L.twistedChainComplex.X n)

The comparison from the unnormalized cubical chains with coefficients in L to the simplicial chains with coefficients in L: a cube c with a coefficient goes to the pushforward along c of the image of the identity cube of the model.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubePushforward_simplexChain {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n m : ℕ} (c : SingularCube (↑X) n) (t : (TopCat.toSSet.obj (cubeModel n)).obj (Opposite.op { len := m })) (r : ULift.{v, 0} ℤ) (a : ↑(L.obj { as := c 0 })) : ((L.twistedCubePushforward c m) (simplexChain t r)) a = r.down • (CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex m ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map (cubeToHom c)).app (Opposite.op { len := m }))) t))) ((CategoryTheory.ConcreteCategory.hom (L.map ((TopCat.Hom.hom (cubeToHom c)).pathClass (cubeModelOrigin n) ((TopCat.simplexMap t) (Opposite.unop (Opposite.op { len := m })).toTopInitialVertex)))) a)

The evaluation formula of the pushforward along a cube on a simplex t of the model with an integral coefficient: the simplex pushed forward along c, with the coefficient transported along the path class inside the image of c. The definition of twistedCubePushforward is not unfolded outside this file, so this is the way to evaluate it on generators.

theorem TauCeti.LocalCoefficientSystem.twistedCubePushforward_apply {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) (m : ℕ) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : ((L.twistedCubePushforward c m) y) a = ((L.twistedPushforward (cubeToHom c) (cubeModelOrigin n) m) y) a

The pushforward along a cube is the twisted pushforward along the cube regarded as a map from the model, from the origin of the model. This is the defining equation of twistedCubePushforward.

theorem TauCeti.LocalCoefficientSystem.twistedCubePushforward_d {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) (m : ℕ) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (cubeModel n)).X (m + 1))) (a : ↑(L.obj { as := c 0 })) : (CategoryTheory.ConcreteCategory.hom (L.twistedChainComplex.d (m + 1) m)) (((L.twistedCubePushforward c (m + 1)) y) a) = ((L.twistedCubePushforward c m) ((CategoryTheory.ConcreteCategory.hom (((singularChains (ULift.{v, 0} ℤ)).obj (cubeModel n)).d (m + 1) m)) y)) a

The pushforward along a cube commutes with the boundaries.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubicalToSingular_ofCube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (L.twistedCubicalToSingular n) ((TwistedCubicalChain.ofCube L c) a) = ((L.twistedCubePushforward c n) (cubicalToSingularGen (ULift.{v, 0} ℤ) n)) a

The comparison on a cube with a coefficient.

theorem TauCeti.LocalCoefficientSystem.twistedCubicalToSingular_ofSubcube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n m : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (a : ↑(L.obj { as := c 0 })) : (L.twistedCubicalToSingular m) ((TwistedCubicalChain.ofSubcube L c ι) a) = ((L.twistedCubePushforward c m) (cubicalToSingularSubcube (ULift.{v, 0} ℤ) n ι)) a

The comparison on a subcube. The image of a subcube c ∘ ι of c, with the coefficient transported inside c, is the pushforward along c of the image of the subcube upCube ∘ ι of the model.

theorem TauCeti.LocalCoefficientSystem.twistedCubePushforward_gen_eq_zero_of_isDegenerate {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {c : SingularCube (↑X) n} (hc : c.IsDegenerate) (a : ↑(L.obj { as := c 0 })) : ((L.twistedCubePushforward c n) (cubicalToSingularGen (ULift.{v, 0} ℤ) n)) a = 0

A degenerate cube goes to zero: it is a degeneracy s ∘ π of a cube of lower dimension, and the corresponding subcube upCube ∘ π of the model is degenerate.

theorem TauCeti.LocalCoefficientSystem.twistedCubicalToSingular_boundary {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (n : ℕ) (x : L.TwistedCubicalChain (n + 1)) : (L.twistedCubicalToSingular n) ((TwistedCubicalChain.boundary L n) x) = (CategoryTheory.ConcreteCategory.hom (L.twistedChainComplex.d (n + 1) n)) ((L.twistedCubicalToSingular (n + 1)) x)

The comparison commutes with the boundaries.

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

The comparison from the normalized cubical chains with coefficients in L to the simplicial chains with coefficients in L: degenerate cubes go to zero.

@[simp]

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_ofCube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (L.normalizedTwistedCubicalToSingular n) ((NormalizedTwistedCubicalChain.ofCube L c) a) = ((L.twistedCubePushforward c n) (cubicalToSingularGen (ULift.{v, 0} ℤ) n)) a

The comparison on the class of a cube with a coefficient.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_ofCube_const {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (x : ↑X) (a : ↑(L.obj { as := x })) : (L.normalizedTwistedCubicalToSingular 0) ((NormalizedTwistedCubicalChain.ofCube L (ContinuousMap.const (Fin 0 → ↑unitInterval) x)) a) = (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

On a point cube, the comparison to simplicial chains is the inclusion of the summand of the point simplex.

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

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap_f {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (n : ℕ) : L.twistedCubicalToSingularMap.f n = ModuleCat.ofHom (L.normalizedTwistedCubicalToSingular n)

The components of the comparison chain map.

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

Naturality in the space of the comparison chain map.

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

Naturality in the local system of the comparison chain map.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_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.normalizedTwistedCubicalToSingular n) (((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom f) z₀ n) y) a) = ((L.twistedPushforward f z₀ n) ((CategoryTheory.ConcreteCategory.hom (((cubicalToSingular (ULift.{v, 0} ℤ)).app Z).f n)) y)) a

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

Pushforwards along simplices and cubes

noncomputable def TauCeti.LocalCoefficientSystem.simplexPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (m : ℕ) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : ↑(L.twistedChainComplex.X m)

The simplicial pushforward along a simplex ρ from the initial vertex of the model, with the coefficient at the initial vertex of ρ.

noncomputable def TauCeti.LocalCoefficientSystem.simplexCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (m : ℕ) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : L.NormalizedTwistedCubicalChain m

The cubical pushforward along a simplex ρ from the initial vertex of the model, with the coefficient at the initial vertex of ρ.

theorem TauCeti.LocalCoefficientSystem.simplexPushforward_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (m : ℕ) (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : L.simplexPushforward ρ m y a = ((L.twistedPushforward (simplexToHom ρ) { len := n }.toTopInitialVertex m) y) a

The simplicial pushforward along a simplex is the twisted pushforward along the simplex regarded as a map from the model.

theorem TauCeti.LocalCoefficientSystem.simplexCubicalPushforward_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (m : ℕ) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : L.simplexCubicalPushforward ρ m y a = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom (simplexToHom ρ)) { len := n }.toTopInitialVertex m) y) a

The cubical pushforward along a simplex is the cubical pushforward along the simplex regarded as a map from the model.

theorem TauCeti.LocalCoefficientSystem.simplexPushforward_add {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (y y' : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : L.simplexPushforward ρ m (y + y') a = L.simplexPushforward ρ m y a + L.simplexPushforward ρ m y' a

The simplicial pushforward along a simplex is additive in the chain.

theorem TauCeti.LocalCoefficientSystem.simplexPushforward_sub {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (y y' : ↑(((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : L.simplexPushforward ρ m (y - y') a = L.simplexPushforward ρ m y a - L.simplexPushforward ρ m y' a

The simplicial pushforward along a simplex is compatible with differences of chains.

theorem TauCeti.LocalCoefficientSystem.d_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 + 1))) (a : ↑(L.obj (initialVertex ρ))) : (CategoryTheory.ConcreteCategory.hom (L.twistedChainComplex.d (m + 1) m)) (L.simplexPushforward ρ (m + 1) y a) = L.simplexPushforward ρ m ((CategoryTheory.ConcreteCategory.hom (((singularChains (ULift.{v, 0} ℤ)).obj (simplexModel n)).d (m + 1) m)) y) a

The simplicial pushforward along a simplex commutes with the boundaries.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_simplexCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (simplexModel n)).X m)) (a : ↑(L.obj (initialVertex ρ))) : (L.normalizedTwistedCubicalToSingular m) (L.simplexCubicalPushforward ρ m y a) = L.simplexPushforward ρ m ((CategoryTheory.ConcreteCategory.hom (((cubicalToSingular (ULift.{v, 0} ℤ)).app (simplexModel n)).f m)) y) a

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

theorem TauCeti.LocalCoefficientSystem.boundary_simplexCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (ρ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (simplexModel n)).X (m + 1))) (a : ↑(L.obj (initialVertex ρ))) : (NormalizedTwistedCubicalChain.boundary L m) (L.simplexCubicalPushforward ρ (m + 1) y a) = L.simplexCubicalPushforward ρ m ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (simplexModel n)).d (m + 1) m)) y) a

The cubical pushforward along a simplex commutes with the boundaries.

noncomputable def TauCeti.LocalCoefficientSystem.cubeCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) (m : ℕ) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : L.NormalizedTwistedCubicalChain m

The cubical pushforward along a cube c from the origin of the model, with the coefficient at the origin of c: the cubical counterpart of twistedCubePushforward.

theorem TauCeti.LocalCoefficientSystem.cubeCubicalPushforward_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) (m : ℕ) (y : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : L.cubeCubicalPushforward c m y a = ((NormalizedTwistedCubicalChain.pushforward L (TopCat.Hom.hom (cubeToHom c)) (cubeModelOrigin n) m) y) a

The cubical pushforward along a cube is the cubical pushforward along the cube regarded as a map from the model.

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

The cubical pushforward along a cube is additive in the chain.

theorem TauCeti.LocalCoefficientSystem.cubeCubicalPushforward_sub {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n m : ℕ} (c : SingularCube (↑X) n) (y y' : ↑(((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).X m)) (a : ↑(L.obj { as := c 0 })) : L.cubeCubicalPushforward c m (y - y') a = L.cubeCubicalPushforward c m y a - L.cubeCubicalPushforward c m y' a

The cubical pushforward along a cube is compatible with differences of chains.

theorem TauCeti.LocalCoefficientSystem.ofCube_eq_cubeCubicalPushforward {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (NormalizedTwistedCubicalChain.ofCube L c) a = L.cubeCubicalPushforward c n ((cubicalModelPresentation (ULift.{v, 0} ℤ)).gen n) a

A cube with a coefficient is the pushforward along itself of the identity cube of the model.

theorem TauCeti.LocalCoefficientSystem.boundary_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 + 1))) (a : ↑(L.obj { as := c 0 })) : (NormalizedTwistedCubicalChain.boundary L m) (L.cubeCubicalPushforward c (m + 1) y a) = L.cubeCubicalPushforward c m ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).d (m + 1) m)) y) a

The cubical pushforward along a cube commutes with the boundaries.

theorem TauCeti.LocalCoefficientSystem.d_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 + 1))) (a : ↑(L.obj { as := c 0 })) : (CategoryTheory.ConcreteCategory.hom (L.normalizedTwistedCubicalChainComplex.d (m + 1) m)) (L.cubeCubicalPushforward c (m + 1) y a) = L.cubeCubicalPushforward c m ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex (ULift.{v, 0} ℤ)).obj (cubeModel n)).d (m + 1) m)) y) a

The cubical pushforward along a cube commutes with the differentials of the normalized cubical chain complex.

theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalToSingular_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.normalizedTwistedCubicalToSingular m) (L.cubeCubicalPushforward c m y a) = ((L.twistedCubePushforward c m) ((CategoryTheory.ConcreteCategory.hom (((cubicalToSingular (ULift.{v, 0} ℤ)).app (cubeModel n)).f m)) y)) a

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