The retraction of cubical chains onto based chains

Let D be a TauCeti.BasedCubeDeformation n x: a homotopy of every singular cube c of X to an n-based cube, compatible with faces and degeneracies. This file turns D into chain-level data on Massey's normalized cubical chains.

• The end of the homotopy of c is the n-based cube D.retract c. It commutes with faces and preserves degeneracies, so it induces a chain map D.retractChainMap R of normalized cubical chains, whose image is spanned by n-based cubes.
• The homotopy of c, with time as the first coordinate, sweeps out the cube D.sweep c of one dimension more. Its first two faces are c and D.retract c, and its other faces are the swept faces of c. The negative swept-cube operator D.prismChain R therefore satisfies ∂ P + P ∂ = ρ - id, so the swept-cube operator -D.prismChain R is a chain homotopy D.retractHomotopy R from the identity to D.retractChainMap R.

In a dimension m with 0 < m < n, the only n-based m-cube is the constant cube at x, which is degenerate, so the retraction vanishes. As it induces the identity on homology, the normalized cubical homology of X vanishes in these degrees. By the comparison of cubical and simplicial singular chains, so does the singular homology of X: the singular homology of an (n - 1)-connected space vanishes in the positive degrees below n (TauCeti.isZero_singularHomologyFunctor_of_subsingleton_homotopyGroup).

In degree n the retraction lands in the span of the n-based n-cubes, which are the generalized loops of Ω^ (Fin n) X x; this is where the identification of the n-th homology with the homotopy group through the Hurewicz map starts.

Main definitions

• TauCeti.BasedCubeDeformation.retract, TauCeti.BasedCubeDeformation.cubeHomotopy, TauCeti.BasedCubeDeformation.sweep: the end of the deformation of a cube, the deformation as a homotopy, and the cube it sweeps out (its SingularCube.prism).
• TauCeti.BasedCubeDeformation.retractChain, TauCeti.BasedCubeDeformation.prismChain: the induced operators on normalized cubical chains.
• TauCeti.BasedCubeDeformation.retractChainMap, TauCeti.BasedCubeDeformation.retractHomotopy: the retraction as an endomorphism of the normalized cubical chain complex, and the chain homotopy from the identity to it.

Main results

• TauCeti.BasedCubeDeformation.boundary_prismChain_add_prismChain_boundary: the prism identity ∂ P + P ∂ = ρ - id.
• TauCeti.BasedCubeDeformation.retractChain_eq_zero: the retraction vanishes in the positive dimensions below n.
• TauCeti.isZero_homology_normalizedCubicalChainComplex_of_subsingleton_homotopyGroup, TauCeti.isZero_singularHomologyFunctor_of_subsingleton_homotopyGroup: the vanishing of the normalized cubical and of the singular homology of an (n - 1)-connected space in the positive degrees below n.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the deformation of singular chains of an (n - 1)-connected space into the subcomplex of simplices sending the (n - 1)-skeleton to the base point.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for normalized cubical chains and their prism operators.

The end of the deformation and the swept cube

def TauCeti.BasedCubeDeformation.retract {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : SingularCube X m

The n-based cube at the end of the deformation of the singular cube c.

@[simp]

theorem TauCeti.BasedCubeDeformation.retract_apply {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) (y : Fin m → ↑unitInterval) : (D.retract c) y = (D.homotopy c) (1, y)

theorem TauCeti.BasedCubeDeformation.isBased_retract {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : SingularCube.IsBased n x (D.retract c)

The deformation of every cube ends at an n-based cube.

theorem TauCeti.BasedCubeDeformation.retract_of_isBased {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} {c : SingularCube X m} (hc : SingularCube.IsBased n x c) : D.retract c = c

The deformation fixes the n-based cubes.

theorem TauCeti.BasedCubeDeformation.face_retract {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : SingularCube.face i t (D.retract c) = D.retract (SingularCube.face i t c)

The end of the deformation commutes with the faces at the endpoints of the interval.

theorem TauCeti.BasedCubeDeformation.isDegenerateAt_retract {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) : (D.retract c).IsDegenerateAt i

If c does not depend on its coordinate i, then neither does the end of its deformation.

theorem TauCeti.BasedCubeDeformation.isDegenerate_retract {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} {c : SingularCube X m} (hc : c.IsDegenerate) : (D.retract c).IsDegenerate

The end of the deformation of a degenerate cube is degenerate.

theorem TauCeti.BasedCubeDeformation.retract_eq_const {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (hm : m < n) (c : SingularCube X m) : D.retract c = ContinuousMap.const (Fin m → ↑unitInterval) x

In a dimension below n, every cube retracts to the constant cube at x.

def TauCeti.BasedCubeDeformation.cubeHomotopy {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : ContinuousMap.Homotopy c (D.retract c)

The deformation of the singular cube c, as a homotopy from c to D.retract c.

@[simp]

theorem TauCeti.BasedCubeDeformation.cubeHomotopy_apply {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) (p : ↑unitInterval × (Fin m → ↑unitInterval)) : (D.cubeHomotopy c) p = (D.homotopy c) p

def TauCeti.BasedCubeDeformation.sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : SingularCube X (m + 1)

The cube swept out by the deformation of the singular cube c, with time as the first coordinate.

@[simp]

theorem TauCeti.BasedCubeDeformation.sweep_apply {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) (y : Fin (m + 1) → ↑unitInterval) : (D.sweep c) y = (D.homotopy c) (y 0, Fin.tail y)

@[simp]

theorem TauCeti.BasedCubeDeformation.face_zero_zero_sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : SingularCube.face 0 0 (D.sweep c) = c

The swept cube starts at c.

@[simp]

theorem TauCeti.BasedCubeDeformation.face_zero_one_sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X m) : SingularCube.face 0 1 (D.sweep c) = D.retract c

The swept cube ends at the retraction of c.

@[simp]

theorem TauCeti.BasedCubeDeformation.face_succ_sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : SingularCube.face i.succ t (D.sweep c) = D.sweep (SingularCube.face i t c)

The faces of the swept cube in the spatial coordinates are the swept faces.

theorem TauCeti.BasedCubeDeformation.isDegenerateAt_sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) : (D.sweep c).IsDegenerateAt i.succ

If c does not depend on its coordinate i, then its swept cube does not depend on the coordinate i.succ.

theorem TauCeti.BasedCubeDeformation.isDegenerate_sweep {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {m : ℕ} {c : SingularCube X m} (hc : c.IsDegenerate) : (D.sweep c).IsDegenerate

The cube swept out by the deformation of a degenerate cube is degenerate.

The operators on normalized chains

noncomputable def TauCeti.BasedCubeDeformation.retractChain {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] (m : ℕ) : NormalizedCubicalChain X R m →ₗ[R] NormalizedCubicalChain X R m

The retraction onto n-based cubes, on normalized cubical chains.

noncomputable def TauCeti.BasedCubeDeformation.prismChain {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] (m : ℕ) : NormalizedCubicalChain X R m →ₗ[R] NormalizedCubicalChain X R (m + 1)

The negative swept-cube operator on normalized cubical chains.

@[simp]

theorem TauCeti.BasedCubeDeformation.retractChain_ofCube {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] {m : ℕ} (c : SingularCube X m) : (D.retractChain R m) (NormalizedCubicalChain.ofCube X R c) = NormalizedCubicalChain.ofCube X R (D.retract c)

@[simp]

theorem TauCeti.BasedCubeDeformation.prismChain_ofCube {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] {m : ℕ} (c : SingularCube X m) : (D.prismChain R m) (NormalizedCubicalChain.ofCube X R c) = -NormalizedCubicalChain.ofCube X R (D.sweep c)

theorem TauCeti.BasedCubeDeformation.retractChain_mem_span {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] {m : ℕ} (g : NormalizedCubicalChain X R m) : (D.retractChain R m) g ∈ Submodule.span R (NormalizedCubicalChain.ofCube X R '' {c : SingularCube X m | SingularCube.IsBased n x c})

The retraction lands in the span of the n-based cubes.

theorem TauCeti.BasedCubeDeformation.retractChain_eq_zero {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] {m : ℕ} (hm : m + 1 < n) : D.retractChain R (m + 1) = 0

The retraction vanishes in the positive dimensions below n: there, every cube retracts to the constant cube at x, which is degenerate.

theorem TauCeti.BasedCubeDeformation.boundary_retractChain {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] (m : ℕ) (g : NormalizedCubicalChain X R (m + 1)) : (NormalizedCubicalChain.boundary X R m) ((D.retractChain R (m + 1)) g) = (D.retractChain R m) ((NormalizedCubicalChain.boundary X R m) g)

The retraction commutes with the boundary.

theorem TauCeti.BasedCubeDeformation.boundary_prismChain_add_prismChain_boundary {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] (m : ℕ) (g : NormalizedCubicalChain X R (m + 1)) : (NormalizedCubicalChain.boundary X R (m + 1)) ((D.prismChain R (m + 1)) g) + (D.prismChain R m) ((NormalizedCubicalChain.boundary X R m) g) = (D.retractChain R (m + 1)) g - g

The prism identity ∂ P + P ∂ = ρ - id in positive degrees, for the swept-cube operator P and the retraction ρ.

theorem TauCeti.BasedCubeDeformation.boundary_prismChain_zero {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) (R : Type u_2) [Ring R] (g : NormalizedCubicalChain X R 0) : (NormalizedCubicalChain.boundary X R 0) ((D.prismChain R 0) g) = (D.retractChain R 0) g - g

The prism identity ∂ P = ρ - id in degree zero.

The chain homotopy on the normalized cubical chain complex

noncomputable def TauCeti.BasedCubeDeformation.retractChainMap {X : TopCat} {n : ℕ} {x : ↑X} (D : BasedCubeDeformation n x) (R : Type u) [Ring R] : (normalizedCubicalChainComplex R).obj X ⟶ (normalizedCubicalChainComplex R).obj X

The retraction onto n-based cubes, as an endomorphism of the normalized cubical chain complex.

@[simp]

theorem TauCeti.BasedCubeDeformation.retractChainMap_f_apply {X : TopCat} {n : ℕ} {x : ↑X} (D : BasedCubeDeformation n x) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.retractChainMap R).f m)) g = (D.retractChain R m) g

theorem TauCeti.BasedCubeDeformation.normalizedCubicalChainComplexXEquiv_retractChainMap_f_apply {X : TopCat} {n : ℕ} {x : ↑X} (D : BasedCubeDeformation n x) (R : Type u) [Ring R] (m : ℕ) (g : ↑(((normalizedCubicalChainComplex R).obj X).X m)) : (normalizedCubicalChainComplexXEquiv X m) ((CategoryTheory.ConcreteCategory.hom ((D.retractChainMap R).f m)) g) = (D.retractChain R m) ((normalizedCubicalChainComplexXEquiv X m) g)

Under the concrete identification of chain-complex terms, the retraction chain map acts by BasedCubeDeformation.retractChain.

noncomputable def TauCeti.BasedCubeDeformation.retractHomotopy {X : TopCat} {n : ℕ} {x : ↑X} (D : BasedCubeDeformation n x) (R : Type u) [Ring R] : Homotopy (CategoryTheory.CategoryStruct.id ((normalizedCubicalChainComplex R).obj X)) (D.retractChainMap R)

The chain homotopy from the identity to the retraction onto n-based cubes, given in degree m by the swept-cube operator -D.prismChain R m.

@[simp]

theorem TauCeti.BasedCubeDeformation.retractHomotopy_hom_succ {X : TopCat} {n : ℕ} {x : ↑X} (D : BasedCubeDeformation n x) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.retractHomotopy R).hom m (m + 1))) g = -(D.prismChain R m) g

theorem TauCeti.isZero_homology_normalizedCubicalChainComplex_of_subsingleton_homotopyGroup {X : TopCat} {n : ℕ} {x : ↑X} (hX : ∀ k < n, Subsingleton (HomotopyGroup (Fin k) (↑X) x)) (R : Type u) [Ring R] {m : ℕ} (hm0 : m ≠ 0) (hm : m < n) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj X) m)

The normalized cubical homology of an (n - 1)-connected space vanishes in the positive degrees below n. The retraction onto n-based cubes induces the identity on homology, since it is chain homotopic to the identity, and it vanishes in these degrees.

theorem TauCeti.isZero_singularHomologyFunctor_of_subsingleton_homotopyGroup {X : TopCat} {n : ℕ} {x : ↑X} (hX : ∀ k < n, Subsingleton (HomotopyGroup (Fin k) (↑X) x)) (R : Type u) [Ring R] {m : ℕ} (hm0 : m ≠ 0) (hm : m < n) : CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).obj X)

The singular homology of an (n - 1)-connected space vanishes in the positive degrees below n. If π_k(X, x) is trivial for every k < n (for k = 0, if X is path connected), then H_m(X; R) = 0 for 0 < m < n, for every coefficient ring R.