The Hurewicz map #
For a space X with a base point x and a coefficient object R of an abelian category with
coproducts, this file constructs the Hurewicz map
HomotopyGroup.hurewicz R n : π_{n+1}(X, x) → (R ⟶ Hₙ₊₁(X; R))
on Mathlib's cubical homotopy groups HomotopyGroup (Fin (n + 1)) X x. It sends the class of a
generalized loop p : Iⁿ⁺¹ → X, which maps the boundary ∂Iⁿ⁺¹ of the cube to x, to the image
of the generator of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ R under the map of pairs
p : (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, {x}), read in Hₙ₊₁(X; R) through the isomorphism
Hₙ₊₁(X; R) ≅ Hₙ₊₁(X, {x}; R). With C = ModuleCat ℤ and R = ℤ, evaluating the resulting
morphism at 1 gives the classical Hurewicz map π_{n+1}(X, x) → Hₙ₊₁(X; ℤ),
[p] ↦ p_*[Iⁿ⁺¹].
The ingredients are the following.
- The cube pair
TauCeti.cubeBoundaryPair n = (Iⁿ, ∂Iⁿ)is isomorphic to the Euclidean disk pairTauCeti.diskBoundaryPair n = (Dⁿ, Sⁿ⁻¹)(TauCeti.diskBoundaryPairIsoCube), through the affine homeomorphism of the cube onto the closed unit ball of the sup norm and the radial rescaling of that ball onto the Euclidean disk. HenceHₙ(Iⁿ, ∂Iⁿ; R) ≅ R(TauCeti.singularHomologyCubeBoundaryPairIso), transported fromTauCeti.singularHomologyDiskBoundaryPairIso. No choices enter: the disk generator comes from the standard generator of the homology of the boundary sphere, and the homeomorphisms are explicit. These are proved inTauCeti/AlgebraicTopology/Disk.leanandTauCeti/AlgebraicTopology/Singular/DiskSphere.lean. - A generalized loop
p : Ω^ (Fin n) X xis a map of pairs(Iⁿ, ∂Iⁿ) ⟶ (X, {x})(GenLoop.toCubeBoundaryPairHom), and homotopic generalized loops induce homotopic maps of pairs, hence the same map on relative homology (GenLoop.singularHomologyMap_toCubeBoundaryPairHom_eq). - Since a point is contractible,
Hₖ₊₁(X) ⟶ Hₖ₊₁(X, {x})is an isomorphism (TauCeti.singularHomologyIsoOfSubsetSingleton, fromTopPair.isIso_singularHomologyπ_of_contractibleSpace).
The Hurewicz map is natural in based maps (HomotopyGroup.hurewicz_map) and sends the identity
class to zero (HomotopyGroup.hurewicz_one).
It is moreover a group homomorphism (HomotopyGroup.hurewicz_mul), bundled as
HomotopyGroup.hurewiczHom. The product [q] * [p] is represented by a concatenation of p and
q along the first direction of the cube, with a slab 1/4 ≤ z₀ ≤ 1/2 between them sent to the
base point. This concatenation is a map of pairs out of (Iⁿ⁺¹, A), where A is the union of
∂Iⁿ⁺¹ and the slab, and its restrictions to the two halves z₀ ≤ 1/4 and z₀ ≥ 1/2 are
reparametrisations of p and q. So additivity reduces to a pinch identity in Hₖ(Iⁿ⁺¹, A):
the inclusion of (Iⁿ⁺¹, ∂Iⁿ⁺¹) induces the sum of the maps induced by the two halves. Write
A = U ∩ V with U = ∂Iⁿ⁺¹ ∪ {z₀ ≥ 1/4} and V = ∂Iⁿ⁺¹ ∪ {z₀ ≤ 1/2}. Their interiors cover the
cube, so by excision and the long exact sequence of the triple (Iⁿ⁺¹, U, A) a map into
Hₖ(Iⁿ⁺¹, A) is determined by its images in Hₖ(Iⁿ⁺¹, U) and Hₖ(Iⁿ⁺¹, V)
(TopPair.singularHomology_inter_hom_ext). In (Iⁿ⁺¹, U) the inclusion is homotopic to the
left half, while the right half lands in U and induces zero; symmetrically in (Iⁿ⁺¹, V).
The pinch identity is stated for any map of pairs out of (Iⁿ⁺¹, ∂Iⁿ⁺¹) sending the slab into the
subspace (TauCeti.singularHomologyMap_cubeBoundaryPair_eq_add), so it applies to relative cubes
as well.
Main declarations #
GenLoop.toCubeBoundaryPairHom: a generalized loop as a map of pairs(Iⁿ, ∂Iⁿ) ⟶ (X, {x}), the map of pairsTauCeti.cubeBoundaryPairHomof its underlying cube (GenLoop.toCubeBoundaryPairHom_eq_cubeBoundaryPairHom).GenLoop.hurewicz: the Hurewicz class of a generalized loop, characterized byGenLoop.hurewicz_comp_singularHomologyIsoOfSubsetSingleton_hom.HomotopyGroup.hurewicz: the Hurewicz map on homotopy classes.TauCeti.singularHomologyMap_cubeBoundaryPair_eq_add: the pinch identity for maps of pairs out of the cube.HomotopyGroup.hurewicz_mul,HomotopyGroup.hurewiczHom: the Hurewicz map is a homomorphism fromπ_{n+1}(X, x), written additively, to the group of morphismsR ⟶ Hₙ₊₁(X; R).HomotopyGroup.hurewiczIntHom: the integral Hurewicz homomorphismπₙ₊₁(X, x) → Hₙ₊₁(X; ℤ), natural in the space (HomotopyGroup.hurewiczIntHom_map).
References #
- A. Hatcher, Algebraic Topology,
Section 4.2, the Hurewicz maps
πₙ(X, x₀) → Hₙ(X)andπₙ(X, A, x₀) → Hₙ(X, A), defined by pushing forward a generator ofHₙ(Dⁿ, ∂Dⁿ).
A generalized loop p : Ω^ (Fin n) X x, a map Iⁿ → X sending the boundary of the cube to
x, as a map of pairs (Iⁿ, ∂Iⁿ) ⟶ (X, {x}).
Instances For
A generalized loop at x sends the boundary of the cube into the subspace {x} of the pair
(X, {x}).
The map of pairs of a generalized loop is the map of pairs TauCeti.cubeBoundaryPairHom of its
underlying cube.
Postcomposing a generalized loop with a based map postcomposes its map of pairs with the
induced map (X, {x}) ⟶ (Y, {y}).
Homotopic generalized loops induce the same map on relative homology: a homotopy relative
to the boundary of the cube is a homotopy of the maps of pairs (Iⁿ, ∂Iⁿ) ⟶ (X, {x}).
The Hurewicz class of a generalized loop p : Iⁿ⁺¹ → X: the image of the generator
TauCeti.singularHomologyCubeBoundaryPairIso of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) under the map of pairs
p : (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, {x}), read in Hₙ₊₁(X; R) through the isomorphism
TauCeti.singularHomologyIsoOfSubsetSingleton
(GenLoop.hurewicz_comp_singularHomologyIsoOfSubsetSingleton_hom).
Instances For
The Hurewicz class of a generalized loop, followed by the isomorphism
Hₙ₊₁(X; R) ≅ Hₙ₊₁(X, {x}; R), is the image of the generator of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) under the
loop viewed as a map of pairs.
The Hurewicz class of a generalized loop, followed by the isomorphism
Hₙ₊₁(X; R) ≅ Hₙ₊₁(X, {x}; R), is the image of the generator of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) under the
loop viewed as a map of pairs.
Homotopic generalized loops have the same Hurewicz class.
Naturality of the Hurewicz class: for a based map f : (X, x) → (Y, y), the Hurewicz
class of f ∘ p is the image of that of p under f_* : Hₙ₊₁(X; R) ⟶ Hₙ₊₁(Y; R).
The Hurewicz map π_{n+1}(X, x) → (R ⟶ Hₙ₊₁(X; R)), sending the class of a generalized
loop p to its Hurewicz class GenLoop.hurewicz R p: the image of the generator of
Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ R under p : (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, {x}), read in Hₙ₊₁(X; R).
Instances For
Naturality of the Hurewicz map: for a based map f : (X, x) → (Y, y), the Hurewicz class
of f_* a is the image of the Hurewicz class of a under f_* : Hₙ₊₁(X; R) ⟶ Hₙ₊₁(Y; R).
The Hurewicz map sends the identity class to zero.
The Hurewicz map is a homomorphism #
The pinch identity for maps of pairs out of the cube. Let f : (Iᵐ, ∂Iᵐ) ⟶ (Y, B) send
the slab 1/4 ≤ zᵢ ≤ 1/2 into B, and let g and h be its restrictions to the two halves
zᵢ ≤ 1/4 and zᵢ ≥ 1/2 of the complement of the slab, reparametrised along the i-th
coordinate by zᵢ ↦ zᵢ / 4 and zᵢ ↦ (zᵢ + 1) / 2. Then f_* = g_* + h_* on relative singular
homology. This is what makes Hurewicz maps additive.
The Hurewicz map is additive: it sends a product of homotopy classes to the sum of their Hurewicz classes.
The Hurewicz map sends the inverse of a class to the negative of its Hurewicz class.
The Hurewicz homomorphism π_{n+1}(X, x) → (R ⟶ Hₙ₊₁(X; R)), from the homotopy group,
written additively, to the group of morphisms from R to singular homology.
Instances For
The Hurewicz map sends the k-th power of a class to k times its Hurewicz class.
The integral Hurewicz homomorphism πₙ₊₁(X, x) → Hₙ₊₁(X; ℤ), [p] ↦ p_*[Iⁿ⁺¹]: the
Hurewicz homomorphism HomotopyGroup.hurewiczHom with integer coefficients, evaluated at
1 : ℤ.
Instances For
Naturality of the integral Hurewicz homomorphism: for a based map f : (X, x) → (Y, y),
the Hurewicz class of f_* a is the image of the Hurewicz class of a under
f_* : Hₙ₊₁(X; ℤ) → Hₙ₊₁(Y; ℤ).