Pushing cubical chains of a simply connected space into chains with local coefficients

Let L be a local coefficient system on X and f : Z → X a map from a simply connected space, with a base point z₀ : Z. A singular cube d of Z together with a coefficient a ∈ L(f z₀) gives a cube of X with a coefficient: the cube f ∘ d with a transported from f z₀ to its origin along the path class inside the image of f (ContinuousMap.pathClass). Extended to integral normalized cubical chains of Z, this is the twisted pushforward NormalizedTwistedCubicalChain.pushforward L f z₀, the cubical counterpart of TauCeti.LocalCoefficientSystem.twistedPushforward. It commutes with the boundaries, changes source along maps of simply connected spaces by changing the base point, and is natural in the space and in the coefficient system.

Main definitions

• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.pushCube L f z₀ d: the cube f ∘ d with the transported coefficient.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward L f z₀ n: the twisted pushforward of integral normalized cubical n-chains of Z.

Main results

• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward_ofCube: the pushforward of a cube is the composite cube with the transported coefficient.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary_pushforward: it commutes with the boundaries.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward_map: change of the source, with change of base point.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map_pushforward, TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.coefficientMap_pushforward: naturality in the space and in the coefficient 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.TwistedCubicalChain.pushCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] (L : LocalCoefficientSystem R X) (f : C(Z, ↑X)) (z₀ : Z) {m : ℕ} (d : SingularCube Z m) : ↑(L.obj { as := f z₀ }) →ₗ[R] L.TwistedCubicalChain m

The cube f ∘ d of X, with a coefficient at f z₀ transported to its origin along the path class inside the image of f.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.pushCube_apply {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {m : ℕ} (d : SingularCube Z m) (a : ↑(L.obj { as := f z₀ })) : (pushCube L f z₀ d) a = (ofCube L (f.comp d)) ((CategoryTheory.ConcreteCategory.hom (L.map (f.pathClass z₀ (d 0)))) a)

The value of pushCube.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube_pushCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {k m : ℕ} (d : SingularCube Z m) (ι : C(Fin k → ↑unitInterval, Fin m → ↑unitInterval)) (a : ↑(L.obj { as := f z₀ })) : (ofSubcube L (f.comp d) ι) ((CategoryTheory.ConcreteCategory.hom (L.map (f.pathClass z₀ (d 0)))) a) = (pushCube L f z₀ (ContinuousMap.comp d ι)) a

A subcube of a pushed cube is the pushed subcube.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_pushCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {m : ℕ} (d : SingularCube Z (m + 1)) (a : ↑(L.obj { as := f z₀ })) : (boundary L m) ((pushCube L f z₀ d) a) = ∑ i : Fin (m + 1), (-1) ^ ↑i • ((pushCube L f z₀ (SingularCube.face i 0 d)) a - (pushCube L f z₀ (SingularCube.face i 1 d)) a)

The boundary of a pushed cube is the alternating sum of its pushed faces.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.pushCube_mem_degenerate {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {m : ℕ} {d : SingularCube Z m} (hd : d.IsDegenerate) (a : ↑(L.obj { as := f z₀ })) : (pushCube L f z₀ d) a ∈ degenerate L m

A degenerate cube pushes forward to a degenerate chain.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.pushCube_comp {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {Z' : Type u_2} [TopologicalSpace Z'] [SimplyConnectedSpace Z'] (g : C(Z', Z)) (w₀ : Z') {m : ℕ} (d : SingularCube Z' m) (a : ↑(L.obj { as := f z₀ })) : (pushCube L (f.comp g) w₀ d) ((CategoryTheory.ConcreteCategory.hom (L.map (f.pathClass z₀ (g w₀)))) a) = (pushCube L f z₀ (g.comp d)) a

Pushing a cube g ∘ d forward along f is pushing d forward along f ∘ g from the base point w₀, after transporting the coefficient from f z₀ to f (g w₀).

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_pushCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {f : C(Z, ↑X)} {z₀ : Z} {Y : TopCat} (h : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) {m : ℕ} (d : SingularCube Z m) (a : ↑(((pullback h).obj L).obj { as := f z₀ })) : (map h L m) ((pushCube ((pullback h).obj L) f z₀ d) a) = (pushCube L (h.comp f) z₀ d) a

Pushing forward along a map h : X → Y after pushing a cube forward with coefficients in the pulled back system is pushing the cube forward along h ∘ f.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_pushCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {K : LocalCoefficientSystem R X} (η : L ⟶ K) {m : ℕ} (d : SingularCube Z m) (a : ↑(L.obj { as := f z₀ })) : (coefficientMap η m) ((pushCube L f z₀ d) a) = (pushCube K f z₀ d) ((CategoryTheory.ConcreteCategory.hom (η.app { as := f z₀ })) a)

A morphism of local systems acts on a pushed cube through the transported coefficient.

noncomputable def TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] (L : LocalCoefficientSystem R X) (f : C(Z, ↑X)) (z₀ : Z) (n : ℕ) : NormalizedCubicalChain Z (ULift.{v, 0} ℤ) n →ₗ[ULift.{v, 0} ℤ] ↑(L.obj { as := f z₀ }) →ₗ[R] L.NormalizedTwistedCubicalChain n

The twisted pushforward of integral normalized cubical chains of a simply connected space Z along f : Z → X: a cube d with a coefficient a ∈ L(f z₀) goes to the cube f ∘ d with the coefficient transported from f z₀ to its origin.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward_ofCube_eq_mk {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {n : ℕ} (d : SingularCube Z n) (a : ↑(L.obj { as := f z₀ })) : ((pushforward L f z₀ n) (NormalizedCubicalChain.ofCube Z (ULift.{v, 0} ℤ) d)) a = Submodule.Quotient.mk ((TwistedCubicalChain.pushCube L f z₀ d) a)

The twisted pushforward of the class of a cube, as a class of an unnormalized chain.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward_ofCube {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {n : ℕ} (d : SingularCube Z n) (a : ↑(L.obj { as := f z₀ })) : ((pushforward L f z₀ n) (NormalizedCubicalChain.ofCube Z (ULift.{v, 0} ℤ) d)) a = (ofCube L (f.comp d)) ((CategoryTheory.ConcreteCategory.hom (L.map (f.pathClass z₀ (d 0)))) a)

The twisted pushforward of the class of a cube is the class of the composite cube, with the coefficient transported from f z₀ to the origin of the cube.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary_pushforward {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {n : ℕ} (y : NormalizedCubicalChain Z (ULift.{v, 0} ℤ) (n + 1)) (a : ↑(L.obj { as := f z₀ })) : (boundary L n) (((pushforward L f z₀ (n + 1)) y) a) = ((pushforward L f z₀ n) ((NormalizedCubicalChain.boundary Z (ULift.{v, 0} ℤ) n) y)) a

The twisted pushforward commutes with the boundaries.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.pushforward_map {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {Z' : Type u_2} [TopologicalSpace Z'] [SimplyConnectedSpace Z'] (g : C(Z', Z)) (w₀ : Z') {n : ℕ} (y : NormalizedCubicalChain Z' (ULift.{v, 0} ℤ) n) (a : ↑(L.obj { as := f z₀ })) : ((pushforward L f z₀ n) ((NormalizedCubicalChain.map (ULift.{v, 0} ℤ) g n) y)) a = ((pushforward L (f.comp g) w₀ n) y) ((CategoryTheory.ConcreteCategory.hom (L.map (f.pathClass z₀ (g w₀)))) a)

Change of source. Pushing forward the image of a chain under a map g : Z' → Z of simply connected spaces is pushing forward the chain along f ∘ g, from the base point w₀ of Z', after transporting the coefficient from f z₀ to f (g w₀).

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map_pushforward {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {f : C(Z, ↑X)} {z₀ : Z} {Y : TopCat} (h : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) {n : ℕ} (y : NormalizedCubicalChain Z (ULift.{v, 0} ℤ) n) (a : ↑(((pullback h).obj L).obj { as := f z₀ })) : (map h L n) (((pushforward ((pullback h).obj L) f z₀ n) y) a) = ((pushforward L (h.comp f) z₀ n) y) a

The twisted pushforward is natural in the space.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.coefficientMap_pushforward {R : Type u} [Ring R] {X : TopCat} {Z : Type u_1} [TopologicalSpace Z] [SimplyConnectedSpace Z] {L : LocalCoefficientSystem R X} {f : C(Z, ↑X)} {z₀ : Z} {K : LocalCoefficientSystem R X} (η : L ⟶ K) {n : ℕ} (y : NormalizedCubicalChain Z (ULift.{v, 0} ℤ) n) (a : ↑(L.obj { as := f z₀ })) : (coefficientMap η n) (((pushforward L f z₀ n) y) a) = ((pushforward K f z₀ n) y) ((CategoryTheory.ConcreteCategory.hom (η.app { as := f z₀ })) a)

The twisted pushforward is natural in the coefficient system.