The Hurewicz class of the tautological loop of a sphere

The map TauCeti.cubeToSphere : Iⁿ⁺¹ → Sⁿ⁺¹ collapses the boundary of the cube to the north pole N, so it is a generalized loop TauCeti.sphereGenLoop (n + 1) of the sphere at N. This file proves that its Hurewicz class generates the top homology of the sphere: the morphism GenLoop.hurewicz R (sphereGenLoop (n + 1)) : R ⟶ Hₙ₊₁(Sⁿ⁺¹; R) is an isomorphism, for coefficients R in any abelian category with coproducts (TauCeti.isIso_hurewicz_sphereGenLoop). In other words, the quotient map (Iⁿ⁺¹, ∂Iⁿ⁺¹) → (Sⁿ⁺¹, N) sends the fundamental class of the cube to a fundamental class of the sphere, and so induces an isomorphism Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ Hₙ₊₁(Sⁿ⁺¹, N; R) (TauCeti.isIso_singularHomologyMap_toCubeBoundaryPairHom_sphereGenLoop).

Every generalized loop factors through the tautological one (GenLoop.map_toSphere_sphereGenLoop), so this is the universal example of the Hurewicz map: every Hurewicz class is the image of that of the tautological loop (GenLoop.hurewicz_eq_hurewicz_sphereGenLoop_comp), which pins down the Hurewicz map on all spaces up to its value on π_{n+1}(Sⁿ⁺¹). Since a homotopy of generalized loops along a path is a free homotopy of the corresponding maps out of the sphere (TauCeti.GenLoop.HomotopyAlong.homotopic_toSphere), and homotopic maps induce the same map on singular homology, base-point change along a path preserves Hurewicz classes (HomotopyGroup.hurewicz_homotopyGroupTransport), and the images of the integral Hurewicz homomorphisms at two points joined by a path coincide (HomotopyGroup.range_hurewiczIntHom_eq_of_joined). With integer coefficients, the image of the top homology of the sphere under the pointed map of a generalized loop is contained in the cyclic group generated by the Hurewicz class of the loop (GenLoop.singularHomologyMap_toSphere_mem_zmultiples, GenLoop.singularHomologyMap_diskBoundaryMap_mem_zmultiples).

The proof reads the Hurewicz class in the local homology Hₙ₊₁(Sⁿ⁺¹, Sⁿ⁺¹ ∖ {s}) at the south pole s, the image of the centre 0 of the disk Dⁿ⁺¹ under TauCeti.closedBallToSphere, through which TauCeti.cubeToSphere factors.

• The punctured sphere Sⁿ⁺¹ ∖ {s} is contractible, so Hₙ₊₁(Sⁿ⁺¹) ⟶ Hₙ₊₁(Sⁿ⁺¹, Sⁿ⁺¹ ∖ {s}) is an isomorphism.
• The boundary sphere Sⁿ of the disk is a deformation retract of Dⁿ⁺¹ ∖ {0}, so (Dⁿ⁺¹, Sⁿ) ⟶ (Dⁿ⁺¹, Dⁿ⁺¹ ∖ {0}) induces isomorphisms on relative homology (TauCeti.isIso_singularHomologyMap_diskBoundaryPairToComplDiskCenter).
• The collapse map is a homeomorphism from the open ball onto Sⁿ⁺¹ ∖ {N}, and only the centre goes to s. So it is a chart at the centre of the disk, and the local homology comparison TauCeti.singularHomologyComplSingletonIsoOfChart shows that (Dⁿ⁺¹, Dⁿ⁺¹ ∖ {0}) ⟶ (Sⁿ⁺¹, Sⁿ⁺¹ ∖ {s}) induces isomorphisms on relative homology.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Proposition 2.22 (the quotient map of a good pair, here (Dⁿ, ∂Dⁿ) → (Dⁿ / ∂Dⁿ, pt)), Section 4.1, the change of base point for higher homotopy groups, and Section 4.2, the Hurewicz map.

The collapse map on the interior of the disk

The Hurewicz class of the tautological loop

instance TauCeti.isIso_hurewicz_sphereGenLoop (n : ℕ) {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.IsIso (GenLoop.hurewicz R (sphereGenLoop (n + 1)))

The Hurewicz class of the tautological loop generates the top homology of the sphere. The class of TauCeti.cubeToSphere : (Iⁿ⁺¹, ∂Iⁿ⁺¹) → (Sⁿ⁺¹, N) under the Hurewicz map is an isomorphism R ≅ Hₙ₊₁(Sⁿ⁺¹; R): the collapse of the boundary of the cube sends the fundamental class of the cube to a fundamental class of the sphere.

instance TauCeti.isIso_singularHomologyMap_toCubeBoundaryPairHom_sphereGenLoop (n : ℕ) {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.IsIso (TopPair.singularHomologyMap (GenLoop.toCubeBoundaryPairHom (sphereGenLoop (n + 1))) R (n + 1))

The collapse of the boundary of the cube induces an isomorphism on relative homology. The map of pairs TauCeti.cubeToSphere : (Iⁿ⁺¹, ∂Iⁿ⁺¹) → (Sⁿ⁺¹, N) induces an isomorphism Hₙ₊₁(Iⁿ⁺¹, ∂Iⁿ⁺¹; R) ≅ Hₙ₊₁(Sⁿ⁺¹, N; R).

theorem GenLoop.hurewicz_eq_hurewicz_sphereGenLoop_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n : ℕ} {X : Type} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin (n + 1)) X x)) : hurewicz R p = CategoryTheory.CategoryStruct.comp (hurewicz R (TauCeti.sphereGenLoop (n + 1))) (((AlgebraicTopology.singularHomologyFunctor C (n + 1)).obj R).map (TopCat.ofHom (toSphere p)))

Every Hurewicz class is the image of that of the tautological loop: the Hurewicz class of a generalized loop p is the image of the Hurewicz class of TauCeti.sphereGenLoop (n + 1) under (GenLoop.toSphere p)_* : Hₙ₊₁(Sⁿ⁺¹; R) ⟶ Hₙ₊₁(X; R).

@[simp]

theorem HomotopyGroup.hurewicz_homotopyGroupTransport {X : Type} [TopologicalSpace X] {x y : X} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) (γ : Path x y) (a : HomotopyGroup (Fin (n + 1)) X x) : hurewicz R n (TauCeti.homotopyGroupTransport γ a) = hurewicz R n a

The Hurewicz map is invariant under base-point change. Transporting a class of πₙ₊₁(X, x) along a path does not change its Hurewicz class in Hₙ₊₁(X; R).

@[simp]

theorem HomotopyGroup.hurewiczIntHom_homotopyGroupTransport {X : Type} [TopologicalSpace X] {x y : X} (γ : Path x y) {n : ℕ} (a : HomotopyGroup (Fin (n + 1)) X x) : (hurewiczIntHom X y n) (Additive.ofMul (TauCeti.homotopyGroupTransport γ a)) = (hurewiczIntHom X x n) (Additive.ofMul a)

The integral Hurewicz homomorphism is invariant under base-point change.

theorem HomotopyGroup.range_hurewiczIntHom_eq_of_joined {X : Type} [TopologicalSpace X] {x y : X} (h : Joined x y) (n : ℕ) : (hurewiczIntHom X x n).range = (hurewiczIntHom X y n).range

The images of the integral Hurewicz homomorphisms at two points joined by a path coincide.

theorem GenLoop.singularHomologyMap_toSphere_mem_zmultiples {n : ℕ} {X : Type} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin (n + 1)) X x)) (b : ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) (n + 1)).obj ↧ℤ).obj ↧↑(Metric.sphere 0 1))) : (ModuleCat.Hom.hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) (n + 1)).obj ↧ℤ).map (TopCat.ofHom (toSphere p)))) b ∈ AddSubgroup.zmultiples ((ModuleCat.Hom.hom (hurewicz (↧ℤ) p)) 1)

The image of the integral homology of the sphere Sⁿ⁺¹ under the pointed map GenLoop.toSphere p of a generalized loop p is contained in the cyclic group generated by the Hurewicz class of p.

theorem GenLoop.singularHomologyMap_diskBoundaryMap_mem_zmultiples {n : ℕ} {X : TopCat} {x : ↑X} (p : ↑(GenLoop (Fin (n + 1)) (↑X) x)) (b : ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) (n + 1)).obj ↧ℤ).obj (TopCat.diskBoundary (n + 1 + 1)))) : (ModuleCat.Hom.hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) (n + 1)).obj ↧ℤ).map (diskBoundaryMap p))) b ∈ AddSubgroup.zmultiples ((ModuleCat.Hom.hom (hurewicz (↧ℤ) p)) 1)

The image of the integral homology of the boundary sphere ∂𝔻ⁿ⁺² under the attaching map GenLoop.diskBoundaryMap p of a generalized loop p is contained in the cyclic group generated by the Hurewicz class of p.