Unnormalized cubical chains with local coefficients

Let L be a local coefficient system on a space X. The cubical n-chains of X with coefficients in L are the direct sum, over the singular n-cubes c of X, of the fibre of L at the origin c 0 of the cube. The boundary of a cube c carrying a coefficient a is the alternating sum of its faces,

∂ (c, a) = Σᵢ (-1) ^ i ((face i 0 c, a) - (face i 1 c, τᵢ a)),

where τᵢ transports a from the origin of c to the origin of its face face i 1 c along the image under c of a path in the cube. The cube is simply connected, so the path class it transports along is determined by its endpoints (ContinuousMap.pathClass); this is what makes the boundary square to zero, exactly as for constant coefficients. This is the cubical version of the singular chains with local coefficients of TauCeti.AlgebraicTopology.Singular.Twisted.Basic, and the complex on which Serre's spectral sequence of a fibre space is built.

Chains are functorial in the coefficient system (coefficientMap) and in the space: a continuous map f : X → Y sends the chains of X with coefficients in the pulled back system f⁎L to the chains of Y with coefficients in L (map). In degree zero, a cocone s over L, for instance the colimit of L or the module M of a constant system, gives an augmentation C^□_0(X; L) → s.pt which vanishes on boundaries.

Main definitions

• TauCeti.LocalCoefficientSystem.TwistedCubicalChain L n: the cubical n-chains with coefficients in L, with ofCube L c, the inclusion of the summand of a cube.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary L n: the boundary.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap η n, TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map f L n: functoriality in the coefficient system and in the space.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment s: the augmentation into a cocone.

Main results

• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_boundary: ∂ ∘ ∂ = 0.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_boundary, TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_boundary: the boundary is natural.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_id, TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_comp, TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_map: functoriality.
• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_boundary: ε ∘ ∂ = 0.

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 II and XIV.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §7.2.

@[reducible, inline]

abbrev TauCeti.LocalCoefficientSystem.TwistedCubicalChain {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : Type (max v₁ w)

The cubical n-chains with coefficients in a local system L: the direct sum, over the singular n-cubes c, of the fibre of L at the origin of c.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofCube {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) : ↑(L.obj { as := c 0 }) →ₗ[R] L.TwistedCubicalChain n

The inclusion of the summand of a singular cube into the cubical chains.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofCube_eq_lof {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} (c : SingularCube (↑X) n) : ofCube L c = DirectSum.lof R (SingularCube (↑X) n) (fun (c : SingularCube (↑X) n) => ↑(L.obj { as := c 0 })) c

The inclusion of the summand of a singular cube is the direct-sum inclusion.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofCube_congr {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} {c c' : SingularCube (↑X) n} (h : c = c') {a : ↑(L.obj { as := c 0 })} {a' : ↑(L.obj { as := c' 0 })} (ha : a ≍ a') : (ofCube L c) a = (ofCube L c') a'

Equal cubes carrying corresponding coefficients, in the fibres of L at their equal origins, are equal chains.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.desc {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {n : ℕ} {N : Type u_1} [AddCommGroup N] [Module R N] (φ : (c : SingularCube (↑X) n) → ↑(L.obj { as := c 0 }) →ₗ[R] N) : L.TwistedCubicalChain n →ₗ[R] N

The linear map out of the cubical chains with prescribed values on each summand.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.desc_ofCube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {N : Type u_1} [AddCommGroup N] [Module R N] (φ : (c : SingularCube (↑X) n) → ↑(L.obj { as := c 0 }) →ₗ[R] N) (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (desc L φ) ((ofCube L c) a) = (φ c) a

The map with prescribed values on summands restricts to the prescribed map on each summand.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.hom_ext {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {N : Type u_1} [AddCommGroup N] [Module R N] {f g : L.TwistedCubicalChain n →ₗ[R] N} (h : ∀ (c : SingularCube (↑X) n), f ∘ₗ ofCube L c = g ∘ₗ ofCube L c) : f = g

Two linear maps out of the cubical chains agree as soon as they agree on every summand.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.hom_ext_iff {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {N : Type u_1} [AddCommGroup N] [Module R N] {f g : L.TwistedCubicalChain n →ₗ[R] N} : f = g ↔ ∀ (c : SingularCube (↑X) n), f ∘ₗ ofCube L c = g ∘ₗ ofCube L c

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.induction_on {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {P : L.TwistedCubicalChain n → Prop} (x : L.TwistedCubicalChain n) (zero : P 0) (ofCube : ∀ (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })), P ((ofCube L c) a)) (add : ∀ (x y : L.TwistedCubicalChain n), P x → P y → P (x + y)) : P x

Induction on cubical chains: a property of chains which holds for 0, for each cube with a coefficient, and is stable under sums, holds for every chain.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {m n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) : ↑(L.obj { as := c 0 }) →ₗ[R] L.TwistedCubicalChain m

The summand of the subcube c ∘ ι of a cube c, with the coefficient transported from the origin of c to the origin of the subcube along the path class inside c.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube_apply {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {m n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (a : ↑(L.obj { as := c 0 })) : (ofSubcube L c ι) a = (ofCube L (ContinuousMap.comp c ι)) ((CategoryTheory.ConcreteCategory.hom (L.map (ContinuousMap.pathClass c 0 (ι 0)))) a)

A subcube with a coefficient is the summand of the subcube with the transported coefficient.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube_id {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) : ofSubcube L c (ContinuousMap.id (Fin n → ↑unitInterval)) = ofCube L c

The cube itself is the subcube along the identity.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube_comp {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {k m n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (κ : C(Fin k → ↑unitInterval, Fin m → ↑unitInterval)) (a : ↑(L.obj { as := c 0 })) : (ofSubcube L (ContinuousMap.comp c ι) κ) ((CategoryTheory.ConcreteCategory.hom (L.map (ContinuousMap.pathClass c 0 (ι 0)))) a) = (ofSubcube L c (ι.comp κ)) a

A subcube of a subcube is a subcube.

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

The boundary of cubical chains with local coefficients.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_ofCube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) (n + 1)) (a : ↑(L.obj { as := c 0 })) : (boundary L n) ((ofCube L c) a) = ∑ i : Fin (n + 1), (-1) ^ ↑i • ((ofSubcube L c (SingularCube.face i 0 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval)))) a - (ofSubcube L c (SingularCube.face i 1 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval)))) a)

The boundary of a cube is the alternating sum of its faces, the subcubes c ∘ face i t id, with the coefficient transported along the path classes inside the cube to the origins of the faces.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_boundary {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (n : ℕ) : boundary L n ∘ₗ boundary L (n + 1) = 0

The boundary of a boundary vanishes.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) : L.TwistedCubicalChain n →ₗ[R] K.TwistedCubicalChain n

The map of cubical chains induced by a morphism of local coefficient systems.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_ofCube {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (coefficientMap η n) ((ofCube L c) a) = (ofCube K c) ((CategoryTheory.ConcreteCategory.hom (η.app { as := c 0 })) a)

A morphism of local systems acts on the summand of each cube by its component at the origin.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_id {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (n : ℕ) : coefficientMap (CategoryTheory.CategoryStruct.id L) n = LinearMap.id

The identity of a local system induces the identity on cubical chains.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_comp {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) (n : ℕ) : coefficientMap (CategoryTheory.CategoryStruct.comp η θ) n = coefficientMap θ n ∘ₗ coefficientMap η n

A composite of morphisms of local systems induces the composite map on cubical chains.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_ofSubcube {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) {m n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (a : ↑(L.obj { as := c 0 })) : (coefficientMap η m) ((ofSubcube L c ι) a) = (ofSubcube K c ι) ((CategoryTheory.ConcreteCategory.hom (η.app { as := c 0 })) a)

A morphism of local systems sends a subcube with a coefficient to the same subcube with the image coefficient.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_boundary {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) : coefficientMap η n ∘ₗ boundary L n = boundary K n ∘ₗ coefficientMap η (n + 1)

The boundary commutes with the maps induced by a morphism of local systems.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (n : ℕ) : ((pullback f).obj L).TwistedCubicalChain n →ₗ[R] L.TwistedCubicalChain n

The map of cubical chains induced by a continuous map f, from the chains with coefficients in the pulled back system f⁎L to the chains with coefficients in L.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_ofCube {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f : C(↑X, ↑Y)} {L : LocalCoefficientSystem R Y} {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(((pullback f).obj L).obj { as := c 0 })) : (map f L n) ((ofCube ((pullback f).obj L) c) a) = (ofCube L (f.comp c)) a

A continuous map sends the summand of a cube identically onto the summand of the image cube.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_ofSubcube {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f : C(↑X, ↑Y)} {L : LocalCoefficientSystem R Y} {m n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)) (a : ↑(((pullback f).obj L).obj { as := c 0 })) : (map f L m) ((ofSubcube ((pullback f).obj L) c ι) a) = (ofSubcube L (f.comp c) ι) a

A continuous map sends a subcube with a coefficient to the image subcube.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_boundary {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (n : ℕ) : map f L n ∘ₗ boundary ((pullback f).obj L) n = boundary L n ∘ₗ map f L (n + 1)

The boundary is natural.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.coefficientMap_map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f : C(↑X, ↑Y)} {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) (n : ℕ) : coefficientMap η n ∘ₗ map f L n = map f K n ∘ₗ coefficientMap ((pullback f).map η) n

The map induced by a continuous map is natural in the coefficient system.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : map (ContinuousMap.id ↑X) L n = coefficientMap ((pullbackIdIso X).hom.app L) n

The identity map induces on cubical chains the map coming from the identification of a system with its pullback along the identity.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.map_comp {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {Z : TopCat} (f : C(↑X, ↑Y)) (g : C(↑Y, ↑Z)) (L : LocalCoefficientSystem R Z) (n : ℕ) : map (g.comp f) L n = map g L n ∘ₗ map f ((pullback g).obj L) n ∘ₗ coefficientMap ((pullbackCompIso f g).hom.app L) n

A composite of continuous maps induces on cubical chains the composite of the two induced maps, after the identification of the pullback along the composite with the iterated pullback.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) : L.TwistedCubicalChain 0 →ₗ[R] ↑s.pt

The augmentation of the cubical 0-chains into a cocone s over the local system: a point x with a coefficient a goes to the image of a under the leg of s at x. For the colimit cocone it takes values in colimit L; for a constant system with fibre M and the cocone of identities it is the sum of the coefficients.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_ofCube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) (c : SingularCube (↑X) 0) (a : ↑(L.obj { as := c 0 })) : (augment s) ((ofCube L c) a) = (CategoryTheory.ConcreteCategory.hom (s.ι.app { as := c 0 })) a

The augmentation sends a 0-cube, a point, with a coefficient to the image of the coefficient under the leg of the cocone at that point.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_ofSubcube {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) {n : ℕ} (c : SingularCube (↑X) n) (ι : C(Fin 0 → ↑unitInterval, Fin n → ↑unitInterval)) (a : ↑(L.obj { as := c 0 })) : (augment s) ((ofSubcube L c ι) a) = (CategoryTheory.ConcreteCategory.hom (s.ι.app { as := c 0 })) a

The augmentation of a point of a subcube, a vertex of the cube, is the image of the coefficient at the origin of the cube.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_boundary {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) : augment s ∘ₗ boundary L 0 = 0

The augmentation vanishes on boundaries: a path with a coefficient contributes the images of the coefficient at both of its end points, which agree in the cocone.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_coefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (s : CategoryTheory.Limits.Cocone K) : augment s ∘ₗ coefficientMap η 0 = augment ((CategoryTheory.Limits.Cocone.precompose η).obj s)

The augmentation is natural in the coefficient system.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.augment_map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) {L : LocalCoefficientSystem R Y} (s : CategoryTheory.Limits.Cocone L) : augment s ∘ₗ map f L 0 = augment (CategoryTheory.Limits.Cocone.whisker (FundamentalGroupoid.map f) s)

The augmentation is natural in the space.