Pushing 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 simplex σ of Z together with a coefficient a ∈ L(f z₀) gives a twisted simplex of X: the simplex f ∘ σ with the coefficient transported from f z₀ to its initial vertex along the path class inside the image of f (ContinuousMap.pathClass). Extended to integral chains of Z, this is the twisted pushforward twistedPushforward L f z₀. Since Z is simply connected, f^* L is trivialized by these transports, and the twisted pushforward is the composite of this trivialization with the pushforward of twisted chains along f.

It is the tool to turn a natural transformation between singular chain theories, given on contractible models, into one between the corresponding theories with local coefficients: a model chain is pushed forward along a simplex or cube, carrying the coefficient of the generator.

Main definitions

• TauCeti.LocalCoefficientSystem.twistedPushforward L f z₀ n: the twisted pushforward of integral singular n-chains of Z.

Main results

• TauCeti.LocalCoefficientSystem.twistedPushforward_simplexChain: its value on a simplex.
• TauCeti.LocalCoefficientSystem.twistedPushforward_d: it commutes with the boundaries.
• TauCeti.LocalCoefficientSystem.twistedPushforward_map: change of the source along a map of simply connected spaces, with change of base point.
• TauCeti.LocalCoefficientSystem.twistedChainComplexMap_twistedPushforward, TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap_twistedPushforward: 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.twistedPushforward {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] (L : LocalCoefficientSystem R X) (f : Z ⟶ X) (z₀ : ↑Z) (n : ℕ) : ↑(((singularChains (ULift.{v, 0} ℤ)).obj Z).X n) →ₗ[ULift.{v, 0} ℤ] ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ }) →ₗ[R] ↑(L.twistedChainComplex.X n)

The twisted pushforward of integral singular chains of a simply connected space Z along f : Z ⟶ X: a simplex σ with a coefficient a ∈ L(f z₀) goes to the twisted simplex f ∘ σ with the coefficient transported from f z₀ to its initial vertex.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedPushforward_simplexChain {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] {L : LocalCoefficientSystem R X} {f : Z ⟶ X} {z₀ : ↑Z} {n : ℕ} (σ : (TopCat.toSSet.obj Z).obj (Opposite.op { len := n })) (r : ULift.{v, 0} ℤ) (a : ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : ((L.twistedPushforward f z₀ n) (simplexChain σ r)) a = r.down • (CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex n ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) σ))) ((CategoryTheory.ConcreteCategory.hom (L.map ((TopCat.Hom.hom f).pathClass z₀ ((TopCat.simplexMap σ) (Opposite.unop (Opposite.op { len := n })).toTopInitialVertex)))) a)

The twisted pushforward of a simplex.

theorem TauCeti.LocalCoefficientSystem.twistedPushforward_simplexChain_one {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] {L : LocalCoefficientSystem R X} {f : Z ⟶ X} {z₀ : ↑Z} {n : ℕ} (σ : (TopCat.toSSet.obj Z).obj (Opposite.op { len := n })) : (L.twistedPushforward f z₀ n) (simplexChain σ 1) = ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (L.map ((TopCat.Hom.hom f).pathClass z₀ ((TopCat.simplexMap σ) (Opposite.unop (Opposite.op { len := n })).toTopInitialVertex))) (L.ιTwistedChainComplex n ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) σ)))

The twisted pushforward of a simplex with coefficient 1, as a morphism of modules.

theorem TauCeti.LocalCoefficientSystem.map_pathClass_self_apply {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {Z' : Type u_1} [TopologicalSpace Z'] [SimplyConnectedSpace Z'] (g : C(Z', ↑X)) (z : Z') (b : ↑(L.obj { as := g z })) : (CategoryTheory.ConcreteCategory.hom (L.map (g.pathClass z z))) b = b

Transport along the path class from a point to itself is the identity.

theorem TauCeti.LocalCoefficientSystem.map_pathClass_heq {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {Z' : Type u_1} [TopologicalSpace Z'] [SimplyConnectedSpace Z'] (g : C(Z', ↑X)) {z z' : Z'} (h : z' = z) (b : ↑(L.obj { as := g z })) : (CategoryTheory.ConcreteCategory.hom (L.map (g.pathClass z z'))) b ≍ b

Transport along the path class to a point equal to the starting point does not change the coefficient, up to the identification of the fibres.

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_eq_twistedPushforward {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (b : ↑(L.obj (initialVertex σ))) : (CategoryTheory.ConcreteCategory.hom (L.ιTwistedChainComplex n σ)) b = ((L.twistedPushforward (simplexToHom σ) { len := n }.toTopInitialVertex n) (simplexChain (idSimplex n) 1)) b

Every twisted simplex is the pushforward along itself of the identity simplex of the model, from the initial vertex of the model.

theorem TauCeti.LocalCoefficientSystem.twistedPushforward_d {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] {L : LocalCoefficientSystem R X} {f : Z ⟶ X} {z₀ : ↑Z} {n : ℕ} (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj Z).X (n + 1))) (a : ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : (CategoryTheory.ConcreteCategory.hom (L.twistedChainComplex.d (n + 1) n)) (((L.twistedPushforward f z₀ (n + 1)) y) a) = ((L.twistedPushforward f z₀ n) ((CategoryTheory.ConcreteCategory.hom (((singularChains (ULift.{v, 0} ℤ)).obj Z).d (n + 1) n)) y)) a

The twisted pushforward commutes with the boundaries.

theorem TauCeti.LocalCoefficientSystem.twistedPushforward_map {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] {L : LocalCoefficientSystem R X} {f : Z ⟶ X} {z₀ : ↑Z} {Z' : TopCat} [SimplyConnectedSpace ↑Z'] (g : Z' ⟶ Z) (w₀ : ↑Z') {n : ℕ} (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj Z').X n)) (a : ↑(L.obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : ((L.twistedPushforward f z₀ n) ((CategoryTheory.ConcreteCategory.hom (((singularChains (ULift.{v, 0} ℤ)).map g).f n)) y)) a = ((L.twistedPushforward (CategoryTheory.CategoryStruct.comp g f) w₀ n) y) ((CategoryTheory.ConcreteCategory.hom (L.map ((TopCat.Hom.hom f).pathClass z₀ ((CategoryTheory.ConcreteCategory.hom 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 g ≫ f, from the base point w₀ of Z', after transporting the coefficient from f z₀ to f (g w₀).

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_twistedPushforward {R : Type u} [Ring R] {X Z : TopCat} [SimplyConnectedSpace ↑Z] {f : Z ⟶ X} {z₀ : ↑Z} {Y : TopCat} (L : LocalCoefficientSystem R Y) (h : X ⟶ Y) {n : ℕ} (y : ↑(((singularChains (ULift.{v, 0} ℤ)).obj Z).X n)) (a : ↑(((pullback (TopCat.Hom.hom h)).obj L).obj { as := (CategoryTheory.ConcreteCategory.hom f) z₀ })) : (CategoryTheory.ConcreteCategory.hom ((twistedChainComplexMap h L).f n)) (((((pullback (TopCat.Hom.hom h)).obj L).twistedPushforward f z₀ n) y) a) = ((L.twistedPushforward (CategoryTheory.CategoryStruct.comp f h) z₀ n) y) a

The twisted pushforward is natural in the space: pushing forward into Y along h after pushing forward into X with coefficients in the pulled back system is pushing forward along f ≫ h.

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

The twisted pushforward is natural in the coefficient system.