The cubical Hurewicz homomorphism

A generalized loop p : Ω^ (Fin (n + 1)) X x is a singular (n + 1)-cube of X sending the boundary of the cube to x, so all of its faces are the constant cube at x (GenLoop.face_eq_const) and it is a cycle of the normalized cubical chains (GenLoop.boundary_ofCube_eq_zero). Its class in normalized cubical homology is the cubical Hurewicz class GenLoop.cubicalHurewicz R p, for any coefficient ring R.

This file shows that the cubical Hurewicz class only depends on the homotopy class of p and that it turns the product of π_{n+1}(X, x) into the sum of homology classes, so that it defines a homomorphism

HomotopyGroup.cubicalHurewiczHom R n : π_{n+1}(X, x) →+ H^□ₙ₊₁(X; R),

natural in based maps (HomotopyGroup.cubicalHurewicz_map). Both facts are witnessed by explicit cubes of one dimension more.

• A homotopy H relative to the boundary from p to q sweeps out an (n + 2)-cube (TauCeti.SingularCube.prism), with time as the first coordinate. Its two faces in the first coordinate are p and q, and all of its other faces are constant, so its boundary is p - q.
• Mathlib represents the product [p] * [q] by the concatenation f = transAt 0 q p, which runs q on the first half of the first coordinate and p on the second half. Precomposing f with the reparametrisation (s, t, w) ↦ (s / 2 + t (1 - s / 2), w) gives an (n + 2)-cube whose faces are f and p for s = 0, 1, q and the constant cube for t = 0, 1, and constant cubes in the remaining coordinates. Constant cubes of positive dimension are degenerate, so its boundary is f - p - q in the normalized chains.

In normalized cubical chains a generalized loop is itself a cycle, with no choice of representative or of a generator of the homology of the cube. This makes the cubical Hurewicz map the form of the Hurewicz map suited to chain-level arguments, such as Eilenberg's deformation of the singular chains of an (n - 1)-connected space into combinations of generalized loops.

Main definitions

• GenLoop.cubicalHurewicz R p: the class of a generalized loop in normalized cubical homology, characterized by GenLoop.homologyπ_eq_cubicalHurewicz.
• HomotopyGroup.cubicalHurewicz R n: the induced map on π_{n+1}(X, x).
• HomotopyGroup.cubicalHurewiczHom R n: the same map, as a homomorphism from π_{n+1}(X, x) written additively.

Main results

• GenLoop.cubicalHurewicz_eq_of_homotopic: homotopic generalized loops have the same class.
• HomotopyGroup.cubicalHurewicz_mul: the cubical Hurewicz map is additive.
• GenLoop.cubicalHurewicz_map, HomotopyGroup.cubicalHurewicz_map: naturality in based maps.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for singular cubes and normalized cubical chains.
• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the comparison of homotopy and homology through singular chains sending a skeleton to the base point.

theorem GenLoop.face_eq_const {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} (p : ↑(GenLoop (Fin (n + 1)) X x)) (i : Fin (n + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : TauCeti.SingularCube.face i t ↑p = ContinuousMap.const (Fin n → ↑unitInterval) x

Every face of a generalized loop, read as a singular cube, is the constant cube at the base point.

theorem GenLoop.boundary_ofCube_eq_zero {X : Type u_1} [TopologicalSpace X] {x : X} {n : ℕ} (R : Type u_2) [Ring R] (p : ↑(GenLoop (Fin (n + 1)) X x)) : (TauCeti.NormalizedCubicalChain.boundary X R n) (TauCeti.NormalizedCubicalChain.ofCube X R ↑p) = 0

A generalized loop is a cycle of the normalized cubical chains.

The cube swept out by a homotopy

The cube relating a concatenation to its two halves

noncomputable def GenLoop.cubicalHurewicz {X : Type u} [TopologicalSpace X] {x : X} {n : ℕ} (R : Type u) [Ring R] (p : ↑(GenLoop (Fin (n + 1)) X x)) : ↑(HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))

The cubical Hurewicz class of a generalized loop p : Iⁿ⁺¹ → X: the class of the cycle p in the normalized cubical homology H^□ₙ₊₁(X; R). It is characterized by GenLoop.homologyπ_eq_cubicalHurewicz.

theorem GenLoop.homologyπ_eq_cubicalHurewicz {X : Type u} [TopologicalSpace X] {x : X} {n : ℕ} (R : Type u) [Ring R] (p : ↑(GenLoop (Fin (n + 1)) X x)) {z : ↑(HomologicalComplex.cycles ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))} (hz : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))) z = TauCeti.NormalizedCubicalChain.ofCube X R ↑p) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))) z = cubicalHurewicz R p

The homology class of any cycle whose underlying chain is the cube p is the cubical Hurewicz class of p.

Homotopy invariance and additivity

theorem GenLoop.cubicalHurewicz_eq_of_homotopic {X : Type u} [TopologicalSpace X] {x : X} {n : ℕ} (R : Type u) [Ring R] {p q : ↑(GenLoop (Fin (n + 1)) X x)} (h : Homotopic p q) : cubicalHurewicz R p = cubicalHurewicz R q

Homotopic generalized loops have the same cubical Hurewicz class.

Naturality

theorem GenLoop.cubicalHurewicz_map {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {n : ℕ} (R : Type u) [Ring R] (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop (Fin (n + 1)) X x)) : cubicalHurewicz R (map f hf p) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((TauCeti.normalizedCubicalChainComplex R).map (TopCat.ofHom f)) (n + 1))) (cubicalHurewicz R p)

Naturality of the cubical Hurewicz class: for a based map f : (X, x) → (Y, y), the cubical Hurewicz class of f ∘ p is the image of that of p under f_*.

noncomputable def HomotopyGroup.cubicalHurewicz {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) : HomotopyGroup (Fin (n + 1)) X x → ↑(HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))

The cubical Hurewicz map π_{n+1}(X, x) → H^□ₙ₊₁(X; R), sending the class of a generalized loop p to the class GenLoop.cubicalHurewicz R p of the cycle p in normalized cubical homology.

@[simp]

theorem HomotopyGroup.cubicalHurewicz_mk {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) (p : ↑(GenLoop (Fin (n + 1)) X x)) : cubicalHurewicz R n ⟦p⟧ = GenLoop.cubicalHurewicz R p

@[simp]

theorem HomotopyGroup.cubicalHurewicz_mul {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) (a b : HomotopyGroup (Fin (n + 1)) X x) : cubicalHurewicz R n (a * b) = cubicalHurewicz R n a + cubicalHurewicz R n b

The cubical Hurewicz map is additive: it sends a product of homotopy classes to the sum of their cubical Hurewicz classes.

@[simp]

theorem HomotopyGroup.cubicalHurewicz_one {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) : cubicalHurewicz R n 1 = 0

The cubical Hurewicz map sends the identity class to zero.

@[simp]

theorem HomotopyGroup.cubicalHurewicz_inv {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) (a : HomotopyGroup (Fin (n + 1)) X x) : cubicalHurewicz R n a⁻¹ = -cubicalHurewicz R n a

The cubical Hurewicz map sends the inverse of a class to the negative of its class.

theorem HomotopyGroup.cubicalHurewicz_map {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (R : Type u) [Ring R] (n : ℕ) (f : C(X, Y)) (hf : f x = y) (a : HomotopyGroup (Fin (n + 1)) X x) : cubicalHurewicz R n (map f hf a) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((TauCeti.normalizedCubicalChainComplex R).map (TopCat.ofHom f)) (n + 1))) (cubicalHurewicz R n a)

Naturality of the cubical Hurewicz map: for a based map f : (X, x) → (Y, y), the cubical Hurewicz class of f_* a is the image of the class of a under f_*.

noncomputable def HomotopyGroup.cubicalHurewiczHom {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) : Additive (HomotopyGroup (Fin (n + 1)) X x) →+ ↑(HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex R).obj ↧X) (n + 1))

The cubical Hurewicz homomorphism π_{n+1}(X, x) → H^□ₙ₊₁(X; R), from the homotopy group written additively to normalized cubical homology.

@[simp]

theorem HomotopyGroup.cubicalHurewiczHom_apply {X : Type u} [TopologicalSpace X] {x : X} (R : Type u) [Ring R] (n : ℕ) (a : Additive (HomotopyGroup (Fin (n + 1)) X x)) : (cubicalHurewiczHom R n) a = cubicalHurewicz R n (Additive.toMul a)