Coherent homotopies of singular cubes

Deformations of all singular cubes of a space, such as TauCeti.BasedCubeDeformation and TauCeti.SubspaceCubeDeformation, are built by induction on the dimension of the cubes. This file holds the part of that induction that does not depend on where the cubes are deformed to.

A TauCeti.CoherentCubeHomotopies X m is a homotopy of every singular m-cube c of X, starting at c, such that

• the homotopy of a cube not depending on a coordinate does not depend on it either;
• for every (m + 1)-cube, the homotopies of its faces agree where two faces meet.

The second property is what lets the homotopies of the faces of an (m + 1)-cube c glue to a homotopy of the restriction of c to the boundary of the cube (TauCeti.CoherentCubeHomotopies.boundaryHomotopy), to be extended over the whole cube. If c does not depend on its coordinate k, its homotopy is instead read off its face in that coordinate (TauCeti.CoherentCubeHomotopies.degenerateHomotopy). Homotopies of the (m + 1)-cubes that restrict on every face to the homotopy of that face are again coherent (TauCeti.CoherentCubeHomotopies.coherent_of_homotopy_insertNth).

The inductive constructions also leave a time window for each dimension in which the homotopies of lower-dimensional cubes are stationary: those of cubes of dimension k are stationary from the time TauCeti.CoherentCubeHomotopies.threshold (k + 1) = (k + 1) / (k + 2) on.

Main definitions and results

• TauCeti.CoherentCubeHomotopies: coherent homotopies of all singular m-cubes.
• TauCeti.CoherentCubeHomotopies.boundaryHomotopy: the homotopy of the boundary of an (m + 1)-cube glued from the homotopies of its faces.
• TauCeti.CoherentCubeHomotopies.degenerateHomotopy: the homotopy of an (m + 1)-cube read off its face in one coordinate.
• TauCeti.CoherentCubeHomotopies.coherent_of_homotopy_insertNth: homotopies of the (m + 1)-cubes compatible with faces are coherent.
• TauCeti.CoherentCubeHomotopies.threshold: the times k / (k + 1) staggering the dimensions.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for singular cubes and their degeneracies.

structure TauCeti.CoherentCubeHomotopies (X : Type u_1) [TopologicalSpace X] (m : ℕ) : Type u_1

Coherent homotopies of the singular m-cubes of X: a homotopy of every singular m-cube c, with time as the first coordinate, starting at c, such that the homotopy of a cube not depending on a coordinate does not depend on it either, and such that for every (m + 1)-cube the homotopies of its faces agree where two faces meet.

• homotopy : SingularCube X m → C(↑unitInterval × (Fin m → ↑unitInterval), X)

  The homotopy of the singular cube c.

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

  The homotopy of c starts at c.

• isDegenerateAt_curry (c : SingularCube X m) (i : Fin m) : 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.

• coherent (c : SingularCube X (m + 1)) (i j : Fin (m + 1)) (t u : ↑unitInterval) : t = 0 ∨ t = 1 → u = 0 ∨ u = 1 → ∀ (z z' : Fin m → ↑unitInterval), i.insertNth t z = j.insertNth u z' → ∀ (s : ↑unitInterval), (self.homotopy (SingularCube.face i t c)) (s, z) = (self.homotopy (SingularCube.face j u c)) (s, z')

  The homotopies of the faces of an (m + 1)-cube agree where two faces meet.

noncomputable def TauCeti.CoherentCubeHomotopies.threshold (k : ℕ) : ↑unitInterval

The time k / (k + 1). The inductive deformations of singular cubes make the homotopies of the cubes of dimension k stationary from time threshold (k + 1) on, strictly before those of the cubes of dimension k + 1, which leaves room for a further deformation in between.

theorem TauCeti.CoherentCubeHomotopies.threshold_lt_succ (k : ℕ) : threshold k < threshold (k + 1)

The thresholds increase strictly with the dimension.

theorem TauCeti.CoherentCubeHomotopies.threshold_lt_one (k : ℕ) : threshold k < 1

Every threshold is strictly before the end of the homotopies.

noncomputable def TauCeti.CoherentCubeHomotopies.boundaryHomotopy {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (c : SingularCube X (m + 1)) : C(↑unitInterval × ↑(Cube.boundary (Fin (m + 1))), X)

The homotopy of the boundary of an (m + 1)-cube glued from the homotopies of its faces.

theorem TauCeti.CoherentCubeHomotopies.boundaryHomotopy_apply {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (c : SingularCube X (m + 1)) (s : ↑unitInterval) (y : ↑(Cube.boundary (Fin (m + 1)))) (j : Fin (m + 1)) (hj : ↑y j = 0 ∨ ↑y j = 1) : (L.boundaryHomotopy c) (s, y) = (L.homotopy (SingularCube.face j (↑y j) c)) (s, j.removeNth ↑y)

The glued boundary homotopy is read off any face containing the point.

@[simp]

theorem TauCeti.CoherentCubeHomotopies.boundaryHomotopy_zero {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (c : SingularCube X (m + 1)) (y : ↑(Cube.boundary (Fin (m + 1)))) : (L.boundaryHomotopy c) (0, y) = c ↑y

The glued boundary homotopy of c starts at the restriction of c to the boundary.

def TauCeti.CoherentCubeHomotopies.degenerateHomotopy {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (c : SingularCube X (m + 1)) (k : Fin (m + 1)) : C(↑unitInterval × (Fin (m + 1) → ↑unitInterval), X)

The homotopy of an (m + 1)-cube c read off its face in the coordinate k, forgetting that coordinate. When c does not depend on its coordinate k, this is a homotopy of c.

@[simp]

theorem TauCeti.CoherentCubeHomotopies.degenerateHomotopy_apply {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (c : SingularCube X (m + 1)) (k : Fin (m + 1)) (s : ↑unitInterval) (y : Fin (m + 1) → ↑unitInterval) : (L.degenerateHomotopy c k) (s, y) = (L.homotopy (SingularCube.face k 0 c)) (s, k.removeNth y)

Unfolding of TauCeti.CoherentCubeHomotopies.degenerateHomotopy.

theorem TauCeti.CoherentCubeHomotopies.degenerateHomotopy_insertNth {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) {c : SingularCube X (m + 1)} {k : Fin (m + 1)} (hk : c.IsDegenerateAt k) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) (s : ↑unitInterval) (z : Fin m → ↑unitInterval) : (L.degenerateHomotopy c k) (s, i.insertNth t z) = (L.homotopy (SingularCube.face i t c)) (s, z)

If c does not depend on its coordinate k, the homotopy read off its face in that coordinate restricts on each face of c to the homotopy of that face.

theorem TauCeti.CoherentCubeHomotopies.isDegenerateAt_curry_degenerateHomotopy {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) {c : SingularCube X (m + 1)} {k j : Fin (m + 1)} (hj : c.IsDegenerateAt j) (s : ↑unitInterval) : SingularCube.IsDegenerateAt ((L.degenerateHomotopy c k).curry s) j

The homotopy read off a face does not depend on any coordinate the cube does not depend on.

theorem TauCeti.CoherentCubeHomotopies.coherent_of_homotopy_insertNth {X : Type u_1} [TopologicalSpace X] {m : ℕ} (L : CoherentCubeHomotopies X m) (G : SingularCube X (m + 1) → C(↑unitInterval × (Fin (m + 1) → ↑unitInterval), X)) (hG : ∀ (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval}, t = 0 ∨ t = 1 → ∀ (s : ↑unitInterval) (z : Fin m → ↑unitInterval), (G c) (s, i.insertNth t z) = (L.homotopy (SingularCube.face i t c)) (s, z)) (c : SingularCube X (m + 1 + 1)) (i j : Fin (m + 1 + 1)) (t u : ↑unitInterval) (ht : t = 0 ∨ t = 1) (hu : u = 0 ∨ u = 1) (z z' : Fin (m + 1) → ↑unitInterval) (h : i.insertNth t z = j.insertNth u z') (s : ↑unitInterval) : (G (SingularCube.face i t c)) (s, z) = (G (SingularCube.face j u c)) (s, z')

Coherence in the next dimension. Homotopies G of the (m + 1)-cubes that restrict on every face of a cube to the homotopy of that face are coherent: for every (m + 2)-cube, the homotopies G of its faces agree where two faces meet.