Deforming singular cubes into based cubes

Let x be a point of a space X. A singular m-cube is n-based at x (TauCeti.SingularCube.IsBased) when it sends the (n - 1)-skeleton of the cube Iᵐ, the points with fewer than n coordinates in the open interval (0, 1), to x. In dimension less than n only the constant cube at x is n-based (TauCeti.SingularCube.isBased_iff_of_lt), and an n-cube is n-based exactly when it is a generalized loop in Ω^ (Fin n) X x (TauCeti.SingularCube.isBased_iff_mem_genLoop). Faces of n-based cubes are n-based.

This file shows that when X is (n - 1)-connected, that is, when π_k(X, x) is trivial for every k < n, every singular cube deforms into an n-based cube, coherently: there is a TauCeti.BasedCubeDeformation, a homotopy of each singular cube c from c to an n-based cube, such that

• the homotopy of a face of c is the restriction of the homotopy of c to that face;
• the homotopy of a cube not depending on a coordinate does not depend on it either;
• the homotopy of an n-based cube is constant.

Conversely such a deformation contracts every generalized loop of dimension k < n relative to the boundary, so it exists exactly when X is (n - 1)-connected (TauCeti.nonempty_basedCubeDeformation_iff).

The n-based cubes span a subcomplex of the normalized cubical chains, and the three properties above are what the prism operators of the homotopies need to define a chain homotopy from the identity to a retraction onto that subcomplex. In positive degrees below n that subcomplex is zero, since the constant cube is degenerate, and in degree n it is spanned by generalized loops; this is how the deformation enters the comparison of homotopy and homology of (n - 1)-connected spaces.

Construction

The homotopies are built by induction on the dimension of the cubes. The homotopy of an n-based cube is constant, and that of a degenerate cube is read off one of its faces. For any other (m + 1)-cube c, the homotopies of the faces of c agree where two faces meet, so they glue to a homotopy of the restriction of c to the boundary of the cube, and the homotopy extension property of the boundary (TauCeti.hasHomotopyExtensionProperty_cubeBoundary) extends it to a homotopy of c. Its end sends the (n - 1)-skeleton to x as soon as m + 1 ≥ n, because the (n - 1)-skeleton then lies in the boundary. When m + 1 < n the whole end must be the constant cube: there the boundary homotopy is constant at x after some time, at which the extension is a generalized loop in Ω^ (Fin (m + 1)) X x; it is contracted, relative to the boundary, using that π_{m + 1}(X, x) is trivial. To leave room for these contractions, the homotopies of cubes of dimension k < n reach x by the increasing times (k + 1) / (k + 2). The gluing of the face homotopies, the homotopies of degenerate cubes and the coherence of each new dimension come from TauCeti.CoherentCubeHomotopies.

Main definitions and results

• TauCeti.SingularCube.IsBased: cubes sending the (n - 1)-skeleton to x.
• TauCeti.BasedCubeDeformation: a coherent deformation of all singular cubes into n-based cubes.
• TauCeti.basedCubeDeformation: such a deformation for an (n - 1)-connected space.
• TauCeti.nonempty_basedCubeDeformation_iff: such a deformation exists exactly when X is (n - 1)-connected.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the subcomplex of singular simplices sending the (n - 1)-skeleton to the base point, of which the n-based cubes are the cubical analogue.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for singular cubes and their degeneracies.

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

A singular m-cube c is n-based at x when it sends the (n - 1)-skeleton of the cube Iᵐ to x: every point of Iᵐ with fewer than n coordinates in the open interval (0, 1) lies on a face of dimension less than n, and is sent to x.

theorem TauCeti.SingularCube.isBased_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} {m : ℕ} {c : SingularCube X m} : IsBased n x c ↔ ∀ (y : Fin m → ↑unitInterval), {i : Fin m | y i ≠ 0 ∧ y i ≠ 1}.card < n → c y = x

Unfolding of TauCeti.SingularCube.IsBased.

@[simp]

theorem TauCeti.SingularCube.isBased_const {X : Type u_1} [TopologicalSpace X] (n : ℕ) (x : X) (m : ℕ) : IsBased n x (ContinuousMap.const (Fin m → ↑unitInterval) x)

The constant cube at x is n-based at x.

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

A face of an n-based cube, at an endpoint of the interval, is n-based.

theorem TauCeti.SingularCube.isBased_iff_of_lt {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} {m : ℕ} (hm : m < n) {c : SingularCube X m} : IsBased n x c ↔ ∀ (y : Fin m → ↑unitInterval), c y = x

In dimension less than n, the only n-based cube is the constant cube at x.

theorem TauCeti.SingularCube.isBased_iff_mem_genLoop {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} {c : SingularCube X n} : IsBased n x c ↔ c ∈ GenLoop (Fin n) X x

An n-cube is n-based at x exactly when it sends the boundary of the cube to x, that is, when it is a generalized loop in Ω^ (Fin n) X x.

Extending the deformation over a single cube

Deforming all cubes of one dimension

The deformation

structure TauCeti.BasedCubeDeformation {X : Type u_1} [TopologicalSpace X] (n : ℕ) (x : X) : Type u_1

A deformation of the singular cubes of X into n-based cubes: a homotopy of every singular cube c, with time as the first coordinate, starting at c and ending at a cube sending the (n - 1)-skeleton to x. The homotopies are compatible with faces and degeneracies, and fix the cubes that are already n-based.

• homotopy {m : ℕ} (c : SingularCube X m) : C(↑unitInterval × (Fin m → ↑unitInterval), X)

  The homotopy deforming the singular cube c.

• homotopy_zero {m : ℕ} (c : SingularCube X m) (y : Fin m → ↑unitInterval) : (self.homotopy c) (0, y) = c y

  The homotopy of c starts at c.

• isBased_curry_one {m : ℕ} (c : SingularCube X m) : SingularCube.IsBased n x ((self.homotopy c).curry 1)

  The homotopy of c ends at an n-based cube.

• homotopy_insertNth {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) (s : ↑unitInterval) (z : Fin m → ↑unitInterval) : (self.homotopy c) (s, i.insertNth t z) = (self.homotopy (SingularCube.face i t c)) (s, z)

  The homotopy of a face of c is the restriction of the homotopy of c to that face.

• isDegenerateAt_curry {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) (s : ↑unitInterval) : SingularCube.IsDegenerateAt ((self.homotopy c).curry s) i

  If c does not depend on a coordinate, then neither does its homotopy at any time.

• homotopy_of_isBased {m : ℕ} {c : SingularCube X m} (hc : SingularCube.IsBased n x c) (s : ↑unitInterval) (y : Fin m → ↑unitInterval) : (self.homotopy c) (s, y) = c y

  The homotopy of an n-based cube is constant.

noncomputable def TauCeti.basedCubeDeformation {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (hX : ∀ k < n, Subsingleton (HomotopyGroup (Fin k) X x)) : BasedCubeDeformation n x

Every singular cube of an (n - 1)-connected space deforms into an n-based cube. If π_k(X, x) is trivial for every k < n (for k = 0, if X is path connected), then there is a deformation of the singular cubes of X into cubes sending the (n - 1)-skeleton to x, compatible with faces and degeneracies and fixing the n-based cubes.

theorem TauCeti.BasedCubeDeformation.homotopic_const {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} (D : BasedCubeDeformation n x) {k : ℕ} (hk : k < n) (p : ↑(GenLoop (Fin k) X x)) : GenLoop.Homotopic p GenLoop.const

A deformation of the singular cubes into n-based cubes deforms every generalized loop of dimension k < n to the constant loop, relative to the boundary of the cube.

theorem TauCeti.nonempty_basedCubeDeformation_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} {x : X} : Nonempty (BasedCubeDeformation n x) ↔ ∀ k < n, Subsingleton (HomotopyGroup (Fin k) X x)

The singular cubes of X deform into n-based cubes exactly when X is (n - 1)-connected: when π_k(X, x) is trivial for every k < n.