Normalized cubical chains with local coefficients

Let L be a local coefficient system on a space X. The degenerate chains with coefficients in L are the sums of the summands of the degenerate cubes, and the normalized cubical chains C^□_n(X; L) are the cubical chains with coefficients in L modulo the degenerate ones. They are the chains with local coefficients of Serre, Homologie singulière des espaces fibrés, Chapter II, in Massey's convention for degeneracy, and they extend the normalized cubical chains of TauCeti.AlgebraicTopology.Singular.Cubical.Normalized from constant coefficients to local ones.

The degenerate chains form a subcomplex. On a cube c which does not depend on its coordinate i, every face of c in another coordinate is degenerate, and the two faces in the coordinate i coincide, with the same transported coefficient: writing c as a degeneracy s ∘ π, both faces are the subcube s of c, and the transport inside c is the transport inside s.

The boundary, the maps induced by morphisms of local systems and by continuous maps, and the augmentation all descend to the normalized chains; the chain complex they form is in TauCeti.AlgebraicTopology.Singular.Cubical.LocalCoefficients.ChainComplex.

Main definitions

• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate L n: the degenerate chains.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain L n: the normalized cubical chains.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary, .coefficientMap, .map, .augment: the induced boundary, functoriality and augmentation.

Main results

• TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_ofCube_mem_degenerate, TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_le_comap_boundary: the degenerate chains form a subcomplex.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary_ofCube: the boundary of a cube, and TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary_boundary: ∂ ∘ ∂ = 0.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.augment_boundary: ε ∘ ∂ = 0.
• TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map_id, TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map_comp: functoriality.

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.

noncomputable def TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : Submodule R (L.TwistedCubicalChain n)

The degenerate n-chains with coefficients in L: the sum of the summands of the degenerate n-cubes.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofCube_mem_degenerate {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 })) : (ofCube L c) a ∈ degenerate L n

A degenerate cube with any coefficient is a degenerate chain.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.ofSubcube_mem_degenerate {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {m n : ℕ} {c : SingularCube (↑X) n} {ι : C(Fin m → ↑unitInterval, Fin n → ↑unitInterval)} (hc : SingularCube.IsDegenerate (ContinuousMap.comp c ι)) (a : ↑(L.obj { as := c 0 })) : (ofSubcube L c ι) a ∈ degenerate L m

A degenerate subcube with any coefficient is a degenerate chain.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_le {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {p : Submodule R (L.TwistedCubicalChain n)} (h : ∀ (c : SingularCube (↑X) n), c.IsDegenerate → ∀ (a : ↑(L.obj { as := c 0 })), (ofCube L c) a ∈ p) : degenerate L n ≤ p

A submodule contains the degenerate chains as soon as it contains every degenerate cube with every coefficient.

@[simp]

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_zero {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : degenerate L 0 = ⊥

There are no degenerate 0-chains: a 0-cube is a point.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.boundary_ofCube_mem_degenerate {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} {c : SingularCube (↑X) (n + 1)} (hc : c.IsDegenerate) (a : ↑(L.obj { as := c 0 })) : (boundary L n) ((ofCube L c) a) ∈ degenerate L n

The boundary of a degenerate cube is a degenerate chain: the two terms of a coordinate the cube does not depend on cancel, and every other face is degenerate.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_le_comap_boundary {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (n : ℕ) : degenerate L (n + 1) ≤ Submodule.comap (boundary L n) (degenerate L n)

The degenerate chains form a subcomplex.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_le_comap_coefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) : degenerate L n ≤ Submodule.comap (coefficientMap η n) (degenerate K n)

A morphism of local systems preserves degenerate chains.

theorem TauCeti.LocalCoefficientSystem.TwistedCubicalChain.degenerate_le_comap_map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (n : ℕ) : degenerate ((pullback f).obj L) n ≤ Submodule.comap (map f L n) (degenerate L n)

A continuous map preserves degenerate chains.

@[reducible, inline]

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

The normalized cubical n-chains with coefficients in a local system L: the cubical chains with coefficients in L modulo the degenerate ones.

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

The class of a singular cube with a coefficient in the normalized chains.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube_apply {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (c : SingularCube (↑X) n) (a : ↑(L.obj { as := c 0 })) : (ofCube L c) a = Submodule.Quotient.mk ((TwistedCubicalChain.ofCube L c) a)

The class of a cube with a coefficient is the class of the corresponding unnormalized chain.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube_eq_zero {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 })) : (ofCube L c) a = 0

A degenerate cube is zero in the normalized chains.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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'

The classes of equal cubes agree on heterogeneously equal coefficients.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain n →ₗ[R] N} (h : ∀ (c : SingularCube (↑X) n), f ∘ₗ ofCube L c = g ∘ₗ ofCube L c) : f = g

Two linear maps out of the normalized chains agree as soon as they agree on every cube.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain n →ₗ[R] N} : f = g ↔ ∀ (c : SingularCube (↑X) n), f ∘ₗ ofCube L c = g ∘ₗ ofCube L c

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

The boundary of normalized cubical chains with coefficients in L.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary_mk {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {n : ℕ} (x : L.TwistedCubicalChain (n + 1)) : (boundary L n) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((TwistedCubicalChain.boundary L n) x)

The boundary of the class of a chain is the class of its boundary.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 • ((ofCube L (ContinuousMap.comp c (SingularCube.face i 0 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))))) ((CategoryTheory.ConcreteCategory.hom (L.map (ContinuousMap.pathClass c 0 ((SingularCube.face i 0 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))) 0)))) a) - (ofCube L (ContinuousMap.comp c (SingularCube.face i 1 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))))) ((CategoryTheory.ConcreteCategory.hom (L.map (ContinuousMap.pathClass c 0 ((SingularCube.face i 1 (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))) 0)))) a))

The boundary of the class of a cube is the alternating sum of the classes of its faces, with the coefficient transported along the path classes inside the cube to the origins of the faces.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain.coefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) : L.NormalizedTwistedCubicalChain n →ₗ[R] K.NormalizedTwistedCubicalChain n

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.coefficientMap_mk {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) {n : ℕ} (x : L.TwistedCubicalChain n) : (coefficientMap η n) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((TwistedCubicalChain.coefficientMap η n) x)

The map induced by a morphism of local systems on the class of a chain.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 class of a cube by its component at the origin.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 normalized chains.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 normalized chains.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain.map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (n : ℕ) : ((pullback f).obj L).NormalizedTwistedCubicalChain n →ₗ[R] L.NormalizedTwistedCubicalChain n

The map of normalized 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.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map_mk {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f : C(↑X, ↑Y)} {L : LocalCoefficientSystem R Y} {n : ℕ} (x : ((pullback f).obj L).TwistedCubicalChain n) : (map f L n) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((TwistedCubicalChain.map f L n) x)

The map induced by a continuous map on the class of a chain.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 class of a cube to the class of the image cube.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain.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 normalized chains the map coming from the identification of a system with its pullback along the identity.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 normalized 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.NormalizedTwistedCubicalChain.augment {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) : L.NormalizedTwistedCubicalChain 0 →ₗ[R] ↑s.pt

The augmentation of the normalized 0-chains into a cocone s over the local system.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.augment_mk {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} (s : CategoryTheory.Limits.Cocone L) (x : L.TwistedCubicalChain 0) : (augment s) (Submodule.Quotient.mk x) = (TwistedCubicalChain.augment s) x

The augmentation of the class of a 0-chain is its augmentation.

@[simp]

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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 of a point with a coefficient is the image of the coefficient in the cocone.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.

theorem TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.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.NormalizedTwistedCubicalChain.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.