Homotopy classes of based cubes and the face relation

An n-cube that is n-based at x is a generalized loop in Ω^ (Fin n) X x (TauCeti.SingularCube.isBased_iff_mem_genLoop), so it has a class in π_n(X, x) (TauCeti.SingularCube.basedClass). For n ≥ 2 these classes assemble into a homomorphism TauCeti.NormalizedCubicalChain.basedClassHom from the normalized integral cubical n-chains to π_n(X, x), sending every cube that is not based to zero; it is well defined on normalized chains because a degenerate based cube is constant.

The main result is the face relation: if an (n + 1)-cube c is n-based at x, its faces are generalized loops, and

Σᵢ (-1) ^ i ([face i 0 c] - [face i 1 c]) = 0 in π_n(X, x),

that is, basedClassHom kills the boundary of c (TauCeti.NormalizedCubicalChain.basedClassHom_boundary_ofCube), and hence the boundary of every combination of based cubes (TauCeti.NormalizedCubicalChain.basedClassHom_boundary_of_mem_span). So a combination of based cubes that is a boundary of based cubes has trivial class. This is the relation needed to invert the Hurewicz map π_n(X, x) → H_n(X; ℤ) of an (n - 1)-connected space, whose singular chains deform into combinations of based cubes.

Proof of the face relation

Write a = k and b = k + 1 for two adjacent coordinates. Precomposing c with the reparametrisation z ↦ z[a ↦ max(z_a, 2 z_b - 1), b ↦ min(1, 2 z_b)] caps the face b = 1: the new cube runs c at double speed in the coordinate b and then the face b = 1, swept along the coordinate a. Its face b = 1 is constant, its face a = 0 is the concatenation of the old face a = 0 with the old face b = 1, and every other face is an old face concatenated with a constant loop. As the face b = 1 has sign -(-1) ^ b = (-1) ^ a in the alternating sum, the sum is unchanged. Reflecting the coordinate b swaps the two faces in that coordinate and reverses every other face in it, which negates the sum. Capping, reflecting and capping again therefore makes both faces in the coordinate b constant without changing whether the sum vanishes. Doing this for b = n, n - 1, …, 1 leaves a cube whose faces outside the first coordinate are all constant; such a cube is a homotopy relative to the boundary between its two faces in the first coordinate, whose classes then agree.

The adjacent coordinates matter: the faces a = 0 and b = 1 share their parametrisation, so the transfer involves no permutation of coordinates.

Main definitions and results

• TauCeti.SingularCube.basedClass: the class in π_n(X, x) of an n-cube that is n-based at x, and of the constant loop for any other cube.
• TauCeti.NormalizedCubicalChain.basedClassHom: the homomorphism from normalized integral cubical (n + 2)-chains to π_{n+2}(X, x).
• TauCeti.NormalizedCubicalChain.basedClassHom_boundary_ofCube and TauCeti.NormalizedCubicalChain.basedClassHom_boundary_of_mem_span: the face relation.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the class in π_n of an n-chain of singular simplices sending the (n - 1)-skeleton to the base point, of which this is the cubical analogue.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for singular cubes, their faces and normalized cubical chains.

The class of a based cube

noncomputable def TauCeti.SingularCube.basedClass {X : Type u_1} [TopologicalSpace X] (x : X) {n : ℕ} (c : SingularCube X n) : HomotopyGroup (Fin n) X x

The class in π_n(X, x) of a singular n-cube that is n-based at x, that is, of a generalized loop at x (TauCeti.SingularCube.isBased_iff_mem_genLoop). Every other n-cube is sent to the class of the constant loop.

theorem TauCeti.SingularCube.basedClass_of_isBased {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X n} (h : IsBased n x c) : basedClass x c = ⟦⟨c, ⋯⟩⟧

theorem TauCeti.SingularCube.basedClass_of_not_isBased {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X n} (h : ¬IsBased n x c) : basedClass x c = ⟦GenLoop.const⟧

@[simp]

theorem TauCeti.SingularCube.basedClass_coe {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} (p : ↑(GenLoop (Fin n) X x)) : basedClass x ↑p = ⟦p⟧

The class of a generalized loop, read as a singular cube, is its homotopy class.

@[simp]

theorem TauCeti.SingularCube.basedClass_const {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} : basedClass x (ContinuousMap.const (Fin n → ↑unitInterval) x) = ⟦GenLoop.const⟧

The constant cube at x has the class of the constant loop.

theorem TauCeti.SingularCube.basedClass_of_isDegenerate {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X n} (hc : c.IsDegenerate) : basedClass x c = ⟦GenLoop.const⟧

A degenerate cube has the class of the constant loop: if it is based, it is constant.

Reparametrising one coordinate

Cubes whose faces are generalized loops

Capping a face

The alternating sum of the classes of the faces

noncomputable def TauCeti.NormalizedCubicalChain.basedClassHom {X : Type u_1} [TopologicalSpace X] (x : X) (n : ℕ) : NormalizedCubicalChain X ℤ (n + 2) →ₗ[ℤ] Additive (HomotopyGroup (Fin (n + 2)) X x)

The homomorphism from the normalized integral cubical (n + 2)-chains of X to π_{n+2}(X, x) that sends the class of an (n + 2)-based cube, a generalized loop, to its homotopy class (TauCeti.SingularCube.basedClass), and the class of every other cube to zero. It is well defined on normalized chains because a degenerate based cube is constant.

@[simp]

theorem TauCeti.NormalizedCubicalChain.basedClassHom_ofCube {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} (c : SingularCube X (n + 2)) : (basedClassHom x n) (ofCube X ℤ c) = Additive.ofMul (SingularCube.basedClass x c)

theorem TauCeti.NormalizedCubicalChain.basedClassHom_ofCube_of_isBased {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X (n + 2)} (hc : SingularCube.IsBased (n + 2) x c) : (basedClassHom x n) (ofCube X ℤ c) = Additive.ofMul ⟦⟨c, ⋯⟩⟧

An (n + 2)-based cube is sent to its class as a generalized loop.

theorem TauCeti.NormalizedCubicalChain.basedClassHom_ofCube_of_not_isBased {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X (n + 2)} (hc : ¬SingularCube.IsBased (n + 2) x c) : (basedClassHom x n) (ofCube X ℤ c) = 0

A cube that is not (n + 2)-based is sent to zero.

theorem TauCeti.NormalizedCubicalChain.basedClassHom_boundary_ofCube {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {c : SingularCube X (n + 3)} (hc : SingularCube.IsBased (n + 2) x c) : (basedClassHom x n) ((boundary X ℤ (n + 2)) (ofCube X ℤ c)) = 0

Boundaries of based cubes have trivial class: the boundary of an (n + 2)-based (n + 3)-cube is sent to zero in π_{n+2}(X, x). Equivalently, the alternating sum of the classes of its faces, which are generalized loops, vanishes.

theorem TauCeti.NormalizedCubicalChain.basedClassHom_boundary_of_mem_span {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} {g : NormalizedCubicalChain X ℤ (n + 3)} (hg : g ∈ Submodule.span ℤ (ofCube X ℤ '' {c : SingularCube X (n + 3) | SingularCube.IsBased (n + 2) x c})) : (basedClassHom x n) ((boundary X ℤ (n + 2)) g) = 0

The boundary of a combination of (n + 2)-based (n + 3)-cubes is sent to zero in π_{n+2}(X, x).