The cone on cubical chains of a contractible space

Let H be a homotopy from the constant map at a point v of a space X to the identity of X. The cone on a singular n-cube c of X is the (n+1)-cube which follows H along a new first coordinate,

cone c (t, x) = H (t, c x).

Its face at t = 1 is c, its face at t = 0 is the constant cube at v, and its faces in the other coordinates are the cones on the faces of c. So, on chains,

∂ (cone f) + cone (∂ f) = [v] - f,

where [v] stands for the constant cube at v with the coefficients of f. In positive degrees the constant cube is degenerate, hence zero in the normalized chains: the negated cone is a contracting homotopy of the normalized cubical chains of X in positive degrees, and in degree zero it contracts onto the multiples of the point v. Consequently the normalized cubical chains of a contractible space are acyclic: every cycle of positive degree is a boundary (NormalizedCubicalChain.exists_boundary_eq_of_boundary_eq_zero), and every 0-chain of augmentation zero is a boundary (NormalizedCubicalChain.exists_boundary_eq_of_augment_eq_zero). Convex sets, in particular the cubes Iⁿ and the topological simplices, are contractible; they are the models of the comparison between cubical and simplicial singular chains, and this is the acyclicity of the cubical side on them.

The cone is degenerate on degenerate cubes (SingularCube.IsDegenerateAt.cone), so it descends to the normalized chains.

Main definitions

• TauCeti.SingularCube.cone: the cone on a singular cube along a contracting homotopy.
• TauCeti.CubicalChain.cone, TauCeti.NormalizedCubicalChain.cone: the cone on unnormalized and on normalized cubical chains.

Main results

• TauCeti.CubicalChain.boundary_cone_add_cone_boundary: ∂ (cone f) + cone (∂ f) = [v] - f.
• TauCeti.NormalizedCubicalChain.boundary_cone_add_cone_boundary: on normalized chains of positive degree, ∂ (cone f) + cone (∂ f) = -f.
• TauCeti.NormalizedCubicalChain.boundary_cone_zero: in degree zero, ∂ (cone f) = ε(f) • [v] - f.
• TauCeti.NormalizedCubicalChain.exists_boundary_eq_of_boundary_eq_zero and TauCeti.NormalizedCubicalChain.exists_boundary_eq_of_augment_eq_zero: the normalized cubical chains of a contractible space are acyclic.

References

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

def TauCeti.SingularCube.cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) : SingularCube X (n + 1)

The cone on a singular n-cube c along a homotopy H from the constant map at v to the identity: the (n+1)-cube (t, x) ↦ H (t, c x), along a new first coordinate t.

@[simp]

theorem TauCeti.SingularCube.cone_apply {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) (x : Fin (n + 1) → ↑unitInterval) : (cone H c) x = H (x 0, c (Fin.tail x))

@[simp]

theorem TauCeti.SingularCube.face_zero_one_cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) : face 0 1 (cone H c) = c

The face of the cone at the new coordinate equal to 1 is the cube itself.

theorem TauCeti.SingularCube.face_zero_zero_cone_apply {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) (x : Fin n → ↑unitInterval) : (face 0 0 (cone H c)) x = v

The face of the cone at the new coordinate equal to 0 is the constant cube at v.

@[simp]

theorem TauCeti.SingularCube.face_succ_cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (j : Fin (n + 1)) (t : ↑unitInterval) (c : SingularCube X (n + 1)) : face j.succ t (cone H c) = cone H (face j t c)

The faces of the cone in the other coordinates are the cones on the faces.

theorem TauCeti.SingularCube.isDegenerate_face_zero_zero_cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X (n + 1)) : (face 0 0 (cone H c)).IsDegenerate

The face of the cone at the new coordinate equal to 0 is degenerate in positive dimensions: it is constant.

theorem TauCeti.SingularCube.IsDegenerateAt.cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} {c : SingularCube X n} {i : Fin n} (h : c.IsDegenerateAt i) : (SingularCube.cone H c).IsDegenerateAt i.succ

The cone on a cube independent of its i-th coordinate is independent of its (i+1)-st.

theorem TauCeti.SingularCube.IsDegenerate.cone {X : Type u_1} [TopologicalSpace X] {v : X} (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} {c : SingularCube X n} (h : c.IsDegenerate) : (SingularCube.cone H c).IsDegenerate

The cone on a degenerate cube is degenerate.

noncomputable def TauCeti.CubicalChain.cone {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) (n : ℕ) : CubicalChain X R n →ₗ[R] CubicalChain X R (n + 1)

The cone on cubical chains along a homotopy from a constant map to the identity, extending SingularCube.cone linearly.

@[simp]

theorem TauCeti.CubicalChain.cone_single {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) (a : R) : (cone R H n) (Finsupp.single c a) = Finsupp.single (SingularCube.cone H c) a

noncomputable def TauCeti.CubicalChain.coneBase {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) (n : ℕ) : CubicalChain X R n →ₗ[R] CubicalChain X R n

The chain of the faces of the cones at the new coordinate equal to 0: the constant cubes at v, with the coefficients of the chain.

@[simp]

theorem TauCeti.CubicalChain.coneBase_single {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) (a : R) : (coneBase R H n) (Finsupp.single c a) = Finsupp.single (SingularCube.face 0 0 (SingularCube.cone H c)) a

theorem TauCeti.CubicalChain.cone_mem_degenerate {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} {f : CubicalChain X R n} (hf : f ∈ degenerate X R n) : (cone R H n) f ∈ degenerate X R (n + 1)

The cone of a degenerate chain is degenerate.

theorem TauCeti.CubicalChain.coneBase_mem_degenerate {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (f : CubicalChain X R (n + 1)) : (coneBase R H (n + 1)) f ∈ degenerate X R (n + 1)

In positive degrees the constant cubes at v are degenerate.

theorem TauCeti.CubicalChain.boundary_cone_zero {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) (f : CubicalChain X R 0) : (boundary X R 0) ((cone R H 0) f) = (coneBase R H 0) f - f

The cone in degree zero: the boundary of the cone on a point is the point v minus the point.

theorem TauCeti.CubicalChain.boundary_cone_add_cone_boundary {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (f : CubicalChain X R (n + 1)) : (boundary X R (n + 1)) ((cone R H (n + 1)) f) + (cone R H n) ((boundary X R n) f) = (coneBase R H (n + 1)) f - f

The cone formula: ∂ (cone f) + cone (∂ f) = [v] - f, where [v] is the chain of the constant cubes at v with the coefficients of f.

noncomputable def TauCeti.NormalizedCubicalChain.cone {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) (n : ℕ) : NormalizedCubicalChain X R n →ₗ[R] NormalizedCubicalChain X R (n + 1)

The cone on normalized cubical chains along a homotopy from a constant map to the identity.

@[simp]

theorem TauCeti.NormalizedCubicalChain.cone_mk {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (f : CubicalChain X R n) : (cone R H n) (Submodule.Quotient.mk f) = Submodule.Quotient.mk ((CubicalChain.cone R H n) f)

@[simp]

theorem TauCeti.NormalizedCubicalChain.cone_ofCube {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (c : SingularCube X n) : (cone R H n) (ofCube X R c) = ofCube X R (SingularCube.cone H c)

theorem TauCeti.NormalizedCubicalChain.boundary_cone_add_cone_boundary {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) {n : ℕ} (f : NormalizedCubicalChain X R (n + 1)) : (boundary X R (n + 1)) ((cone R H (n + 1)) f) + (cone R H n) ((boundary X R n) f) = -f

The contracting homotopy in positive degrees: on normalized chains, ∂ (cone f) + cone (∂ f) = -f.

theorem TauCeti.NormalizedCubicalChain.boundary_cone_zero {X : Type u_1} [TopologicalSpace X] {v : X} (R : Type u_2) [Ring R] (H : (ContinuousMap.const X v).Homotopy (ContinuousMap.id X)) (f : NormalizedCubicalChain X R 0) : (boundary X R 0) ((cone R H 0) f) = (augment X R) f • ofCube X R (SingularCube.point v) - f

The cone in degree zero: ∂ (cone f) = ε(f) • [v] - f.

theorem TauCeti.NormalizedCubicalChain.exists_boundary_eq_of_boundary_eq_zero {X : Type u_1} [TopologicalSpace X] (R : Type u_2) [Ring R] [ContractibleSpace X] {n : ℕ} {f : NormalizedCubicalChain X R (n + 1)} (hf : (boundary X R n) f = 0) : ∃ (g : NormalizedCubicalChain X R (n + 1 + 1)), (boundary X R (n + 1)) g = f

Acyclicity in positive degrees: a cycle of positive degree in the normalized cubical chains of a contractible space is a boundary.

theorem TauCeti.NormalizedCubicalChain.exists_boundary_eq_of_augment_eq_zero {X : Type u_1} [TopologicalSpace X] (R : Type u_2) [Ring R] [ContractibleSpace X] {f : NormalizedCubicalChain X R 0} (hf : (augment X R) f = 0) : ∃ (g : NormalizedCubicalChain X R (0 + 1)), (boundary X R 0) g = f

Acyclicity in degree zero: a 0-chain of augmentation zero in the normalized cubical chains of a contractible space is a boundary.