Path-connectedness of the cube and its boundary

Mathlib's higher homotopy groups π_ n X x are built from generalized loops Ω^ N X x, continuous maps I^N → X sending the cube boundary Cube.boundary N ({y | ∃ i, y i = 0 ∨ y i = 1}) to the base point. Reasoning about π_ n for n ≥ 2 needs to know how the cube and, crucially, its boundary are connected: the boundary of an n-cube is the topological sphere S^{n-1}, which is connected precisely when n ≥ 2. Mathlib records the cube boundary set but proves nothing about its connectivity.

This file supplies that missing input:

• the whole cube I^N is path connected (TauCeti.isPathConnected_cube);
• its boundary is path connected as soon as the index type has at least two elements (TauCeti.isPathConnected_cubeBoundary).

The resulting path-connectedness declarations expose JoinedIn witnesses through their .joinedIn methods, so callers can use the generic connectedness API directly.

The paths are elementary: a coordinate is dragged to 0 along the straight line pathTowardZero, and any boundary point is joined to the corner 0 in two phases that each keep one coordinate pinned at an endpoint, so the whole journey stays inside the boundary. The two-element hypothesis is exactly what lets the second phase pin a different coordinate at 0 while releasing the first.

Main declarations

• TauCeti.pathTowardZero: the straight-line path in I from a to 0.
• TauCeti.isPathConnected_cube: I^N is path connected.
• TauCeti.zero_mem_cubeBoundary: the corner 0 lies on the boundary.
• TauCeti.isPathConnected_cubeBoundary: for [Nontrivial N], Cube.boundary N is path connected.

def TauCeti.pathTowardZero (a : ↑unitInterval) : Path a 0

The straight-line path in the unit interval I from a to 0, given by t ↦ a * σ t where σ is the interval symmetry t ↦ 1 - t.

Equations

• TauCeti.pathTowardZero a = { toFun := fun (t : ↑unitInterval) => a * unitInterval.symm t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem TauCeti.pathTowardZero_apply (a t : ↑unitInterval) : (pathTowardZero a) t = a * unitInterval.symm t

theorem TauCeti.isPathConnected_cube {N : Type u_1} : IsPathConnected Set.univ

The cube I^N is path connected: every point is joined to the corner 0 by the pointwise product of the coordinate paths pathTowardZero.

theorem TauCeti.zero_mem_cubeBoundary {N : Type u_1} [Nonempty N] : 0 ∈ Cube.boundary N

The corner 0 lies on the boundary of the cube (any coordinate is 0).

theorem TauCeti.isPathConnected_cubeBoundary {N : Type u_1} [Nontrivial N] : IsPathConnected (Cube.boundary N)

The boundary of the cube I^N is path connected once the index type has at least two elements. Any boundary point y, extreme in some coordinate i₀, is joined to the corner 0 in two phases: first collapse every other coordinate to 0 (keeping i₀ extreme), then collapse the i₀-coordinate (keeping a different coordinate j₀ at 0). The two-element hypothesis provides the index j₀ ≠ i₀.