Unnormalized cubical chains

The unnormalized cubical n-chains of a space X with coefficients in a ring R are the formal R-combinations of singular n-cubes, SingularCube X n →₀ R. The boundary of an (n+1)-cube is the alternating sum of its faces,

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

following Massey, Singular Homology Theory, Chapter II, and it satisfies ∂ ∘ ∂ = 0. Chains push forward along continuous maps, and the boundary is natural.

Chains are modelled concretely, as finitely supported functions on a type, rather than as a chain complex in an abstract preadditive category: the normalized cubical chains built on top of this file are the quotient of this module by the degenerate cubes, and the constructions on them (products, actions) are maps between such carriers. The coefficient ring need not be commutative: only the central signs (-1) ^ i enter the boundary.

Main definitions

• TauCeti.CubicalChain X R n: unnormalized cubical n-chains.
• TauCeti.CubicalChain.boundary X R n: the boundary CubicalChain X R (n + 1) →ₗ[R] CubicalChain X R n.
• TauCeti.CubicalChain.map R f n: the chains pushed forward along a continuous map.
• TauCeti.CubicalChain.cast R h: reindexing of chains along an equality of dimensions.

Main results

• TauCeti.CubicalChain.boundary_boundary: ∂ ∘ ∂ = 0.
• TauCeti.CubicalChain.map_boundary: the boundary is natural.

Implementation notes

The concrete model, with its boundary and boundary_boundary, follows TauCeti.AlgebraicTopology.Singular.Subdivision.AffineChain.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II.

@[reducible, inline]

abbrev TauCeti.CubicalChain (X : Type u_4) [TopologicalSpace X] (R : Type u_5) [Semiring R] (n : ℕ) : Type (max u_5 u_4)

The unnormalized cubical n-chains of X with coefficients in R: formal R-combinations of singular n-cubes.

noncomputable def TauCeti.CubicalChain.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) (n : ℕ) : CubicalChain X R n →ₗ[R] CubicalChain Y R n

Cubical chains pushed forward along a continuous map.

theorem TauCeti.CubicalChain.map_apply_comp_of_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) (hf : Function.Injective ⇑f) {n : ℕ} (g : CubicalChain X R n) (c : SingularCube X n) : ((map R f n) g) (f.comp c) = g c

An injective map of spaces preserves the coefficient of each cube at its image.

theorem TauCeti.CubicalChain.map_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) (hf : Function.Injective ⇑f) (n : ℕ) : Function.Injective ⇑(map R f n)

An injective continuous map induces an injective push-forward on cubical chains.

@[simp]

theorem TauCeti.CubicalChain.map_single {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) {n : ℕ} (c : SingularCube X n) (a : R) : (map R f n) (Finsupp.single c a) = Finsupp.single (f.comp c) a

@[simp]

theorem TauCeti.CubicalChain.map_id {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] (n : ℕ) : map R (ContinuousMap.id X) n = LinearMap.id

theorem TauCeti.CubicalChain.map_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (R : Type u_4) [Semiring R] (g : C(Y, Z)) (f : C(X, Y)) (n : ℕ) : map R (g.comp f) n = map R g n ∘ₗ map R f n

noncomputable def TauCeti.CubicalChain.cast {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n m : ℕ} (h : n = m) : CubicalChain X R n →ₗ[R] CubicalChain X R m

Reindex cubical chains along an equality of dimensions.

@[simp]

theorem TauCeti.CubicalChain.cast_single {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n m : ℕ} (h : n = m) (c : SingularCube X n) (a : R) : (cast R h) (Finsupp.single c a) = Finsupp.single (SingularCube.cast h c) a

@[simp]

theorem TauCeti.CubicalChain.cast_rfl {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n : ℕ} (f : CubicalChain X R n) : (cast R ⋯) f = f

@[simp]

theorem TauCeti.CubicalChain.cast_cast {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n m k : ℕ} (h : n = m) (h' : m = k) (f : CubicalChain X R n) : (cast R h') ((cast R h) f) = (cast R ⋯) f

Reindexing along successive dimension equalities is reindexing along their composite.

theorem TauCeti.CubicalChain.map_cast {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) {n m : ℕ} (h : n = m) (c : CubicalChain X R n) : (map R f m) ((cast R h) c) = (cast R h) ((map R f n) c)

Reindexing commutes with the push-forward.

noncomputable def TauCeti.CubicalChain.boundaryCube {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X (n + 1)) : CubicalChain X R n

The boundary of a single (n+1)-cube, as an n-chain: ∂ c = Σᵢ (-1) ^ i (face i 0 c - face i 1 c).

theorem TauCeti.CubicalChain.boundaryCube_def {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X (n + 1)) : boundaryCube R c = ∑ i : Fin (n + 1), (-1) ^ ↑i • (Finsupp.single (SingularCube.face i 0 c) 1 - Finsupp.single (SingularCube.face i 1 c) 1)

noncomputable def TauCeti.CubicalChain.boundary (X : Type u_1) [TopologicalSpace X] (R : Type u_4) [Ring R] (n : ℕ) : CubicalChain X R (n + 1) →ₗ[R] CubicalChain X R n

The boundary of cubical chains, ∂ c = Σᵢ (-1) ^ i (face i 0 c - face i 1 c) on a cube, extended linearly.

theorem TauCeti.CubicalChain.boundary_single_one {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X (n + 1)) : (boundary X R n) (Finsupp.single c 1) = boundaryCube R c

The boundary of a cube with coefficient one is boundaryCube.

@[simp]

theorem TauCeti.CubicalChain.boundary_single {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X (n + 1)) (a : R) : (boundary X R n) (Finsupp.single c a) = ∑ i : Fin (n + 1), (-1) ^ ↑i • (Finsupp.single (SingularCube.face i 0 c) a - Finsupp.single (SingularCube.face i 1 c) a)

def TauCeti.CubicalChain.faceSwap {n : ℕ} (p : Fin (n + 2) × Fin (n + 1)) : Fin (n + 2) × Fin (n + 1)

The involution on pairs of face indices behind ∂ ∘ ∂ = 0: (i, j) goes to (i.succAbove j, j.predAbove i).

theorem TauCeti.CubicalChain.faceSwap_def {n : ℕ} (p : Fin (n + 2) × Fin (n + 1)) : faceSwap p = (p.1.succAbove p.2, p.2.predAbove p.1)

The coordinate formula for the face-index involution faceSwap.

theorem TauCeti.CubicalChain.faceSwap_faceSwap {n : ℕ} (p : Fin (n + 2) × Fin (n + 1)) : faceSwap (faceSwap p) = p

theorem TauCeti.CubicalChain.faceSwap_ne {n : ℕ} (p : Fin (n + 2) × Fin (n + 1)) : faceSwap p ≠ p

theorem TauCeti.CubicalChain.boundary_boundary {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] (n : ℕ) : boundary X R n ∘ₗ boundary X R (n + 1) = 0

The boundary of a boundary vanishes.

theorem TauCeti.CubicalChain.map_boundary {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) (n : ℕ) : map R f n ∘ₗ boundary X R n = boundary Y R n ∘ₗ map R f (n + 1)

The boundary is natural.