The relative Hurewicz map #
For a based pair X = (X, A, a₀) and a coefficient object R of an abelian category with
coproducts, this file constructs the relative Hurewicz map
TauCeti.RelHomotopyGroup.hurewicz R n : π_{n+1}(X, A, a₀) → (R ⟶ Hₙ₊₁(X, A; R))
on the relative homotopy sets TauCeti.RelHomotopyGroup (Fin n) X, in every degree n + 1 ≥ 1.
A relative cube p : I × Iⁿ → X sends the face {0} × Iⁿ into A and the rest of the boundary
to a₀ ∈ A. Read on Iⁿ⁺¹ through z ↦ (z 0, Fin.tail z), so that the first coordinate is the
distinguished direction, it is therefore a map of pairs (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A)
(TauCeti.RelGenLoop.toCubeBoundaryPairHom). The relative Hurewicz class of p is the image under
this map of the generator of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ R
(TauCeti.singularHomologyCubeBoundaryPairIso), the generator that also defines the absolute
Hurewicz map HomotopyGroup.hurewicz. With C = ModuleCat ℤ and R = ℤ, evaluating at 1 gives
the classical map π_{n+1}(X, A, a₀) → Hₙ₊₁(X, A; ℤ), [p] ↦ p_*[Iⁿ⁺¹].
A homotopy through relative cubes is a homotopy of maps of pairs, so the class only depends on the
relative homotopy class. The map is natural in morphisms of based pairs and sends the distinguished
class to zero. It extends the absolute Hurewicz map: regarding an absolute class of
π_{n+1}(X, a₀) as a relative class and then applying the relative Hurewicz map agrees with
applying the absolute Hurewicz map and then the quotient map Hₙ₊₁(X; R) ⟶ Hₙ₊₁(X, A; R)
(TauCeti.RelHomotopyGroup.hurewicz_ofHomotopyGroup). The absolute Hurewicz map is defined on
classes modelled on I^(Fin (n + 1)), while TauCeti.RelHomotopyGroup.ofHomotopyGroup takes
classes modelled on I^(Option (Fin n)); the two are matched by finSuccEquiv n, which sends the
first coordinate to the distinguished coordinate none.
In degrees n + 2 ≥ 2, where π_{n+2}(X, A, a₀) is a group, the relative Hurewicz map is a
homomorphism (TauCeti.RelHomotopyGroup.hurewicz_mul). The product [q] * [p] is represented by
a concatenation of p and q along a direction of Iⁿ⁺¹ other than the distinguished one, with
a slab between them sent to a₀, and the pinch identity
TauCeti.singularHomologyMap_cubeBoundaryPair_eq_add, which also gives additivity of the absolute
Hurewicz map, splits its relative Hurewicz class into those of p and q.
Main declarations #
TauCeti.singularHomologyMap_cubeBoundaryPairHom_eq: maps(I × Iⁿ, ∂(I × Iⁿ)) → (X, A)homotopic through maps of pairs induce the same mapHₖ(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ⟶ Hₖ(X, A; R).TauCeti.RelGenLoop.toCubeBoundaryPairHom: a relative cube as a map of pairs(Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A).TauCeti.RelGenLoop.hurewicz: the relative Hurewicz class of a relative cube.TauCeti.RelHomotopyGroup.hurewicz: the relative Hurewicz map on relative homotopy classes, natural byTauCeti.RelHomotopyGroup.hurewicz_map.TauCeti.RelHomotopyGroup.hurewicz_ofHomotopyGroup: compatibility with the absolute Hurewicz map.TauCeti.RelHomotopyGroup.hurewicz_mul,TauCeti.RelHomotopyGroup.hurewiczHom: the relative Hurewicz map is a homomorphism fromπ_{n+2}(X, A, a₀), written additively, to the group of morphismsR ⟶ Hₙ₊₂(X, A; R).TauCeti.RelHomotopyGroup.hurewiczIntHom: with integer coefficients, the relative Hurewicz homomorphism evaluated at1,π_{n+2}(X, A, a₀) → Hₙ₊₂(X, A; ℤ).
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 relative cube sends the boundary of the cube into the subspace.
A relative cube, read on Iⁿ⁺¹ through cubeSplitHomeomorph, sends the boundary of the cube
into the subspace.
A relative cube p : I × Iⁿ → X, read on Iⁿ⁺¹ with the first coordinate as the distinguished
direction, as a map of pairs (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A).
Instances For
Maps of pairs out of the cube that are homotopic through maps of pairs induce the same map
on relative homology: if g₀, g₁ : (I × Iⁿ, ∂(I × Iⁿ)) → (X, A) are homotopic through maps of
pairs, then so are the maps of pairs (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A) they induce.
Homotopic relative cubes induce the same map on relative homology: a homotopy through
relative cubes is a homotopy of the maps of pairs (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A).
Postcomposing a relative cube with a morphism of based pairs postcomposes its map of pairs.
The relative Hurewicz class of a relative cube p : I × Iⁿ → X: the image of the generator
TauCeti.singularHomologyCubeBoundaryPairIso of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) under the map of pairs
p : (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A).
Instances For
Homotopic relative cubes have the same relative Hurewicz class.
Naturality of the relative Hurewicz class: for a morphism of based pairs f, the relative
Hurewicz class of f ∘ p is the image of that of p under
f_* : Hₙ₊₁(X, A; R) ⟶ Hₙ₊₁(Y, B; R).
The relative Hurewicz class of a relative cube with values in the subspace is zero.
Additivity #
The relative Hurewicz map π_{n+1}(X, A, a₀) → (R ⟶ Hₙ₊₁(X, A; R)), sending the class of a
relative cube p to its relative Hurewicz class TauCeti.RelGenLoop.hurewicz R p: the image of
the generator of Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ R under p : (Iⁿ⁺¹, ∂Iⁿ⁺¹) ⟶ (X, A).
Instances For
Naturality of the relative Hurewicz map in morphisms of based pairs.
The relative Hurewicz map sends the distinguished class to zero.
The relative Hurewicz map sends the identity class to zero.
The relative Hurewicz map is additive in degrees at least two: it sends a product of relative homotopy classes to the sum of their relative Hurewicz classes.
The relative Hurewicz map sends the inverse of a class to the negative of its relative Hurewicz class.
The relative Hurewicz homomorphism π_{n+2}(X, A, a₀) → (R ⟶ Hₙ₊₂(X, A; R)), from the
relative homotopy group, written additively, to the group of morphisms from R to relative
singular homology.
Instances For
The relative Hurewicz homomorphism with integer coefficients
π_{n+2}(X, A, a₀) → Hₙ₊₂(X, A; ℤ), [p] ↦ p_*[Iⁿ⁺²]: the relative Hurewicz homomorphism with
coefficients ℤ, evaluated at 1.
Instances For
The relative Hurewicz map extends the absolute one: the relative Hurewicz class of an
absolute class a ∈ π_{n+1}(X, a₀), regarded as a relative class, is the image of the Hurewicz
class of a under Hₙ₊₁(X; R) ⟶ Hₙ₊₁(X, A; R). The absolute class is modelled on Iⁿ⁺¹ and
the relative class on I × Iⁿ, matched by finSuccEquiv n : Fin (n + 1) ≃ Option (Fin n).