The cube modulo its boundary is a sphere

Mathlib's homotopy groups π_ n X x are built from generalized loops, maps I^n → X sending the boundary of the cube to x. The classical description of πₙ(X, x) is by pointed maps (Sⁿ, s₀) → (X, x) from the sphere, and the two are related by the homeomorphism Iⁿ / ∂Iⁿ ≅ Sⁿ. This file constructs that homeomorphism, for the unit sphere of EuclideanSpace ℝ (Fin (n + 1)) pointed at its north pole e_last, and transfers generalized loops, their homotopies and their homotopy classes to pointed maps out of the sphere.

The map from the Euclidean closed unit ball of ℝⁿ to the unit sphere of ℝⁿ⁺¹ is x ↦ (2 √(1 - ‖x‖²) x, 2 ‖x‖² - 1), the last coordinate being the height (TauCeti.closedBallToSphere). It sends the centre to the south pole -e_last, collapses the boundary sphere to the north pole e_last, and is injective on the open ball. The cube map TauCeti.cubeToSphere precomposes it with the homeomorphism TauCeti.diskHomeomorphCube of the disk onto the cube, the one through which TauCeti.cubeBoundaryPair and the Hurewicz maps are compared with the disk. In positive dimension it is surjective, hence a quotient map since the cube is compact, and it induces the homeomorphism TauCeti.cubeQuotientHomeomorphSphere : Iⁿ / ∂Iⁿ ≃ₜ Sⁿ, where Iⁿ / ∂Iⁿ is the quotient by the relation TauCeti.cubeBoundarySetoid identifying all boundary points.

A generalized loop p therefore descends to a pointed map GenLoop.toSphere p out of the sphere, and GenLoop.sphereEquiv identifies generalized loops with pointed maps. Two generalized loops are homotopic relative to the boundary of the cube exactly when the corresponding maps are homotopic relative to the north pole (GenLoop.homotopic_iff_toSphere), so πₙ(X, x) is the set of pointed homotopy classes of maps (Sⁿ, e_last) → (X, x) (HomotopyGroup.sphereEquiv). The identification is natural in based maps (GenLoop.toSphere_map). A class is trivial exactly when its map out of the sphere is null-homotopic, by a free homotopy that need not fix the north pole (HomotopyGroup.mk_eq_one_iff_nullhomotopic_toSphere).

Main declarations

• TauCeti.sphereNorthPole: the north pole e_last of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)).
• TauCeti.closedBallToSphere: the closed unit ball of ℝⁿ modulo its boundary is the sphere, with TauCeti.closedBallToSphere_eq_closedBallToSphere_iff and TauCeti.closedBallToSphere_surjective.
• TauCeti.cubeToSphere: the same for the cube I^n, a quotient map in positive dimension (TauCeti.isQuotientMap_cubeToSphere) collapsing exactly the boundary (TauCeti.cubeToSphere_eq_cubeToSphere_iff, TauCeti.cubeToSphere_eq_sphereNorthPole_iff).
• TauCeti.liftProdCubeToSphere: a family of maps out of the cube, parametrised by I and constant on the boundary at each time, as a family of maps out of the sphere.
• TauCeti.cubeQuotientHomeomorphSphere: the pointed homeomorphism Iⁿ / ∂Iⁿ ≃ₜ Sⁿ.
• TauCeti.sphereGenLoop: TauCeti.cubeToSphere as a generalized loop of the sphere.
• GenLoop.toSphere and GenLoop.sphereEquiv: generalized loops are pointed maps out of the sphere; p is the image of TauCeti.sphereGenLoop under GenLoop.toSphere p (GenLoop.map_toSphere_sphereGenLoop).
• GenLoop.diskBoundaryMap: the map GenLoop.toSphere p with its source written as Mathlib's sphere TopCat.diskBoundary (n + 1), the attaching map of a cell killing ⟦p⟧.
• GenLoop.diskMap: a generalized loop γ of dimension n read on the disk 𝔻 n, the map onto γ of a sphere formed by attaching an n-cell along a constant map.
• GenLoop.homotopic_iff_toSphere and HomotopyGroup.sphereEquiv: homotopy relative to the boundary of the cube is homotopy relative to the north pole, and πₙ(X, x) is the set of pointed homotopy classes of maps Sⁿ → X, the classes of TauCeti.pointedHomotopySetoid.
• TauCeti.GenLoop.HomotopyAlong.homotopic_toSphere: a homotopy of generalized loops along a path is a free homotopy of the corresponding maps out of the sphere.
• HomotopyGroup.mk_eq_one_iff_nullhomotopic_toSphere: a class is trivial exactly when the corresponding map Sⁿ → X is freely null-homotopic.

References

• A. Hatcher, Algebraic Topology, Section 4.1, where πₙ(X, x₀) is described both by maps (Iⁿ, ∂Iⁿ) → (X, x₀) and, through Iⁿ / ∂Iⁿ = Sⁿ, by maps (Sⁿ, s₀) → (X, x₀).

noncomputable def TauCeti.sphereNorthPole (n : ℕ) : ↑(Metric.sphere 0 1)

The north pole e_last of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)): the last standard basis vector.

@[simp]

theorem TauCeti.coe_sphereNorthPole (n : ℕ) : ↑(sphereNorthPole n) = EuclideanSpace.single (Fin.last n) 1

theorem TauCeti.eq_sphereNorthPole_iff {n : ℕ} {y : ↑(Metric.sphere 0 1)} : y = sphereNorthPole n ↔ (↑y).ofLp (Fin.last n) = 1

A point of the unit sphere is the north pole exactly when its height is one.

theorem TauCeti.apply_last_lt_one_iff_ne_sphereNorthPole {n : ℕ} {y : ↑(Metric.sphere 0 1)} : (↑y).ofLp (Fin.last n) < 1 ↔ y ≠ sphereNorthPole n

A point of the unit sphere has height less than one exactly when it is not the north pole.

noncomputable def TauCeti.closedBallToSphere (n : ℕ) : C(↑(Metric.closedBall 0 1), ↑(Metric.sphere 0 1))

The closed unit ball modulo its boundary is the sphere. The map from the closed unit ball of ℝⁿ to the unit sphere of ℝⁿ⁺¹ sending x to (2 √(1 - ‖x‖²) x, 2 ‖x‖² - 1), the last coordinate being the height. It sends the centre to the south pole, collapses the boundary sphere to the north pole (TauCeti.closedBallToSphere_eq_sphereNorthPole_iff), is injective on the open ball (TauCeti.closedBallToSphere_eq_closedBallToSphere_iff) and is surjective in positive dimension (TauCeti.closedBallToSphere_surjective).

@[simp]

theorem TauCeti.closedBallToSphere_apply_castSucc {n : ℕ} (x : ↑(Metric.closedBall 0 1)) (i : Fin n) : (↑((closedBallToSphere n) x)).ofLp i.castSucc = 2 * √(1 - ‖↑x‖ ^ 2) * (↑x).ofLp i

@[simp]

theorem TauCeti.closedBallToSphere_apply_last {n : ℕ} (x : ↑(Metric.closedBall 0 1)) : (↑((closedBallToSphere n) x)).ofLp (Fin.last n) = 2 * ‖↑x‖ ^ 2 - 1

theorem TauCeti.closedBallToSphere_eq_sphereNorthPole_iff {n : ℕ} {x : ↑(Metric.closedBall 0 1)} : (closedBallToSphere n) x = sphereNorthPole n ↔ ‖↑x‖ = 1

TauCeti.closedBallToSphere sends exactly the boundary sphere to the north pole.

theorem TauCeti.closedBallToSphere_eq_closedBallToSphere_iff {n : ℕ} {x y : ↑(Metric.closedBall 0 1)} : (closedBallToSphere n) x = (closedBallToSphere n) y ↔ x = y ∨ ‖↑x‖ = 1 ∧ ‖↑y‖ = 1

TauCeti.closedBallToSphere identifies exactly the points of the boundary sphere: it is injective on the open ball, and its value there is not the north pole.

theorem TauCeti.closedBallToSphere_surjective {n : ℕ} [NeZero n] : Function.Surjective ⇑(closedBallToSphere n)

TauCeti.closedBallToSphere is surjective in positive dimension: the north pole is the image of the boundary sphere, which is nonempty, and every other point of the sphere has an explicit preimage in the open ball.

noncomputable def TauCeti.cubeToSphere (n : ℕ) : C(Fin n → ↑unitInterval, ↑(Metric.sphere 0 1))

The cube modulo its boundary is the sphere. The map from the cube I^n to the unit sphere of EuclideanSpace ℝ (Fin (n + 1)) given by TauCeti.closedBallToSphere after the inverse of the homeomorphism TauCeti.diskHomeomorphCube of the Euclidean disk onto the cube. It collapses exactly the boundary of the cube, to the north pole (TauCeti.cubeToSphere_eq_sphereNorthPole_iff, TauCeti.cubeToSphere_eq_cubeToSphere_iff), and is a quotient map in positive dimension (TauCeti.isQuotientMap_cubeToSphere).

theorem TauCeti.cubeToSphere_apply {n : ℕ} (y : Fin n → ↑unitInterval) : (cubeToSphere n) y = (closedBallToSphere n) ((diskHomeomorphCube n).symm y).down

theorem TauCeti.cubeToSphere_eq_sphereNorthPole_iff {n : ℕ} {y : Fin n → ↑unitInterval} : (cubeToSphere n) y = sphereNorthPole n ↔ y ∈ Cube.boundary (Fin n)

TauCeti.cubeToSphere sends exactly the boundary of the cube to the north pole.

theorem TauCeti.cubeToSphere_eq_cubeToSphere_iff {n : ℕ} {y z : Fin n → ↑unitInterval} : (cubeToSphere n) y = (cubeToSphere n) z ↔ y = z ∨ y ∈ Cube.boundary (Fin n) ∧ z ∈ Cube.boundary (Fin n)

TauCeti.cubeToSphere identifies exactly the points of the boundary of the cube.

noncomputable def TauCeti.sphereGenLoop (n : ℕ) : ↑(GenLoop (Fin n) (↑(Metric.sphere 0 1)) (sphereNorthPole n))

The tautological generalized loop of the sphere: TauCeti.cubeToSphere, which sends the boundary of the cube to the north pole, as a generalized loop at the north pole. Every generalized loop p is its image under the pointed map GenLoop.toSphere p (GenLoop.map_toSphere_sphereGenLoop).

@[simp]

theorem TauCeti.sphereGenLoop_apply {n : ℕ} (y : Fin n → ↑unitInterval) : (sphereGenLoop n) y = (cubeToSphere n) y

theorem TauCeti.cubeToSphere_surjective (n : ℕ) [NeZero n] : Function.Surjective ⇑(cubeToSphere n)

TauCeti.cubeToSphere is surjective in positive dimension.

theorem TauCeti.isQuotientMap_cubeToSphere (n : ℕ) [NeZero n] : Topology.IsQuotientMap ⇑(cubeToSphere n)

TauCeti.cubeToSphere is a quotient map in positive dimension: it is a continuous surjection from the compact cube onto the Hausdorff sphere.

theorem TauCeti.isQuotientMap_prodMap_cubeToSphere (n : ℕ) [NeZero n] : Topology.IsQuotientMap ⇑((ContinuousMap.id ↑unitInterval).prodMap (cubeToSphere n))

The product of the identity of I with TauCeti.cubeToSphere is a quotient map in positive dimension, as a continuous surjection from a compact space onto a Hausdorff space.

noncomputable def TauCeti.liftProdCubeToSphere {n : ℕ} {X : Type u_1} [TopologicalSpace X] [NeZero n] (F : C(↑unitInterval × (Fin n → ↑unitInterval), X)) (hF : ∀ (t : ↑unitInterval), ∀ y ∈ Cube.boundary (Fin n), ∀ z ∈ Cube.boundary (Fin n), F (t, y) = F (t, z)) : C(↑unitInterval × ↑(Metric.sphere 0 1), X)

A family of maps out of the cube, parametrised by I and constant on the boundary of the cube at each time, as a family of maps out of the sphere: the map I × Sⁿ → X through which it factors along TauCeti.cubeToSphere (TauCeti.liftProdCubeToSphere_apply). It turns homotopies of generalized loops, and homotopies of them along paths, into homotopies of maps out of the sphere.

@[simp]

theorem TauCeti.liftProdCubeToSphere_apply {n : ℕ} {X : Type u_1} [TopologicalSpace X] [NeZero n] (F : C(↑unitInterval × (Fin n → ↑unitInterval), X)) (hF : ∀ (t : ↑unitInterval), ∀ y ∈ Cube.boundary (Fin n), ∀ z ∈ Cube.boundary (Fin n), F (t, y) = F (t, z)) (t : ↑unitInterval) (z : Fin n → ↑unitInterval) : (liftProdCubeToSphere F hF) (t, (cubeToSphere n) z) = F (t, z)

noncomputable def TauCeti.cubeQuotientHomeomorphSphere (n : ℕ) [NeZero n] : Quotient (cubeBoundarySetoid (Fin n)) ≃ₜ ↑(Metric.sphere 0 1)

The cube modulo its boundary is homeomorphic to the sphere, by the map induced by TauCeti.cubeToSphere. It is pointed: the class of the boundary goes to the north pole.

@[simp]

theorem TauCeti.cubeQuotientHomeomorphSphere_mk {n : ℕ} [NeZero n] (y : Fin n → ↑unitInterval) : (cubeQuotientHomeomorphSphere n) ⟦y⟧ = (cubeToSphere n) y

theorem TauCeti.cubeQuotientHomeomorphSphere_mk_of_mem_boundary {n : ℕ} [NeZero n] {y : Fin n → ↑unitInterval} (hy : y ∈ Cube.boundary (Fin n)) : (cubeQuotientHomeomorphSphere n) ⟦y⟧ = sphereNorthPole n

TauCeti.cubeQuotientHomeomorphSphere is pointed: it sends the class of the boundary of the cube to the north pole.

@[simp]

theorem TauCeti.cubeQuotientHomeomorphSphere_symm_sphereNorthPole {n : ℕ} [NeZero n] : (cubeQuotientHomeomorphSphere n).symm (sphereNorthPole n) = ⟦0⟧

The inverse of TauCeti.cubeQuotientHomeomorphSphere sends the north pole to the class of the boundary of the cube, represented by its corner 0.

noncomputable def GenLoop.toSphere {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : C(↑(Metric.sphere 0 1), X)

A generalized loop I^n → X, constant on the boundary of the cube, descends along TauCeti.cubeToSphere to a map out of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)) (GenLoop.toSphere_cubeToSphere), sending the north pole to the base point (GenLoop.toSphere_sphereNorthPole).

@[simp]

theorem GenLoop.toSphere_cubeToSphere {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) (z : Fin n → ↑unitInterval) : (toSphere p) ((TauCeti.cubeToSphere n) z) = p z

@[simp]

theorem GenLoop.toSphere_sphereNorthPole {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : (toSphere p) (TauCeti.sphereNorthPole n) = x

@[simp]

theorem GenLoop.toSphere_map {n : ℕ} [NeZero n] {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop (Fin n) X x)) : toSphere (map f hf p) = f.comp (toSphere p)

The pointed map out of the sphere of the image of a generalized loop under a based map is the composite.

@[simp]

theorem GenLoop.map_toSphere_sphereGenLoop {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : map (toSphere p) ⋯ (TauCeti.sphereGenLoop n) = p

Every generalized loop is an image of the tautological loop: p is the image of TauCeti.sphereGenLoop n under the pointed map GenLoop.toSphere p out of the sphere.

@[simp]

theorem GenLoop.toSphere_const {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} : toSphere const = ContinuousMap.const (↑(Metric.sphere 0 1)) x

The constant generalized loop corresponds to the constant map out of the sphere.

noncomputable def GenLoop.sphereEquiv (n : ℕ) [NeZero n] (X : Type u_1) [TopologicalSpace X] (x : X) : ↑(GenLoop (Fin n) X x) ≃ { f : C(↑(Metric.sphere 0 1), X) // f (TauCeti.sphereNorthPole n) = x }

Generalized loops are pointed maps out of the sphere. The bijection between generalized loops (I^n, ∂I^n) → (X, x) and pointed maps (Sⁿ, e_last) → (X, x) out of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)), given by GenLoop.toSphere and by precomposition with TauCeti.cubeToSphere.

@[simp]

theorem GenLoop.coe_sphereEquiv_apply {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : ↑((sphereEquiv n X x) p) = toSphere p

@[simp]

theorem GenLoop.coe_sphereEquiv_symm_apply {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (f : { f : C(↑(Metric.sphere 0 1), X) // f (TauCeti.sphereNorthPole n) = x }) : ↑((sphereEquiv n X x).symm f) = (↑f).comp (TauCeti.cubeToSphere n)

@[simp]

theorem GenLoop.sphereEquiv_symm_apply_apply {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (f : { f : C(↑(Metric.sphere 0 1), X) // f (TauCeti.sphereNorthPole n) = x }) (z : Fin n → ↑unitInterval) : ((sphereEquiv n X x).symm f) z = ↑f ((TauCeti.cubeToSphere n) z)

theorem GenLoop.homotopic_iff_toSphere {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop (Fin n) X x)} : Homotopic p q ↔ (toSphere p).HomotopicRel (toSphere q) {TauCeti.sphereNorthPole n}

Homotopies of generalized loops are pointed homotopies of maps out of the sphere. Two generalized loops are homotopic relative to the boundary of the cube exactly when the corresponding maps out of the sphere are homotopic relative to the north pole.

theorem TauCeti.GenLoop.HomotopyAlong.homotopic_toSphere {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x y : X} {γ : Path x y} {f : ↑(GenLoop (Fin n) X x)} {g : ↑(GenLoop (Fin n) X y)} (h : HomotopyAlong γ f g) : (GenLoop.toSphere f).Homotopic (GenLoop.toSphere g)

A homotopy of generalized loops along a path is a free homotopy of maps out of the sphere. If h is a homotopy from f to g whose boundary traces a path from the base point of f to that of g, then the corresponding maps out of the sphere are homotopic.

noncomputable def GenLoop.diskBoundaryMap {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} (p : ↑(GenLoop (Fin n) (↑X) x)) : TopCat.diskBoundary (n + 1) ⟶ X

The attaching map ∂𝔻 (n + 1) ⟶ X of the (n + 1)-cell that kills the class of a generalized loop p: the pointed map Sⁿ → X corresponding to p (GenLoop.toSphere), with its source written as Mathlib's sphere TopCat.diskBoundary (n + 1).

@[simp]

theorem GenLoop.diskBoundaryMap_apply {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} (p : ↑(GenLoop (Fin n) (↑X) x)) (s : ↑(TopCat.diskBoundary (n + 1))) : (CategoryTheory.ConcreteCategory.hom (diskBoundaryMap p)) s = (toSphere p) s.down

@[simp]

theorem GenLoop.diskBoundaryMap_map {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} {Y : TopCat} (f : X ⟶ Y) {y : ↑Y} (hf : (CategoryTheory.ConcreteCategory.hom f) x = y) (p : ↑(GenLoop (Fin n) (↑X) x)) : diskBoundaryMap (map (TopCat.Hom.hom f) hf p) = CategoryTheory.CategoryStruct.comp (diskBoundaryMap p) f

The attaching map of the image of a generalized loop under a based map is the attaching map of the loop followed by the map.

noncomputable def GenLoop.diskMap {n : ℕ} {X : TopCat} {x : ↑X} (γ : ↑(GenLoop (Fin n) (↑X) x)) : TopCat.disk n ⟶ X

A generalized loop γ of dimension n, read on the disk 𝔻 n through TauCeti.diskHomeomorphCube. When TopCat.diskBoundary n is attached at x along a constant map, this is the map onto γ of the resulting sphere.

@[simp]

theorem GenLoop.diskMap_apply {n : ℕ} {X : TopCat} {x : ↑X} (γ : ↑(GenLoop (Fin n) (↑X) x)) (s : ↑(TopCat.disk n)) : (CategoryTheory.ConcreteCategory.hom (diskMap γ)) s = γ ((TauCeti.diskHomeomorphCube n) s)

@[simp]

theorem GenLoop.diskBoundaryInclusion_comp_diskMap {n : ℕ} {X : TopCat} {x : ↑X} (γ : ↑(GenLoop (Fin n) (↑X) x)) : CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (diskMap γ) = TopCat.ofHom (ContinuousMap.const (ULift.{u, 0} ↑(Metric.sphere 0 1)) x)

A generalized loop at x, read on the disk, is constant at x on the boundary sphere.

@[simp]

theorem GenLoop.diskBoundaryInclusion_comp_diskMap_assoc {n : ℕ} {X : TopCat} {x : ↑X} (γ : ↑(GenLoop (Fin n) (↑X) x)) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (CategoryTheory.CategoryStruct.comp (diskMap γ) h) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.const (ULift.{u, 0} ↑(Metric.sphere 0 1)) x)) h

A generalized loop at x, read on the disk, is constant at x on the boundary sphere.

noncomputable def HomotopyGroup.sphereEquiv (n : ℕ) [NeZero n] (X : Type u_1) [TopologicalSpace X] (x : X) : HomotopyGroup (Fin n) X x ≃ Quotient (TauCeti.pointedHomotopySetoid (TauCeti.sphereNorthPole n) x)

Homotopy groups are pointed homotopy classes of maps out of spheres. The bijection between πₙ(X, x) and the pointed homotopy classes of maps (Sⁿ, e_last) → (X, x) out of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)), induced by GenLoop.sphereEquiv.

@[simp]

theorem HomotopyGroup.sphereEquiv_mk {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : (sphereEquiv n X x) ⟦p⟧ = ⟦(GenLoop.sphereEquiv n X x) p⟧

theorem HomotopyGroup.mk_eq_one_iff_nullhomotopic_toSphere {n : ℕ} [NeZero n] {X : Type u_1} [TopologicalSpace X] {x : X} (p : ↑(GenLoop (Fin n) X x)) : ⟦p⟧ = 1 ↔ (GenLoop.toSphere p).Nullhomotopic

A homotopy class is trivial exactly when its sphere map is null-homotopic. The class of a generalized loop p is the identity of πₙ(X, x) if and only if the corresponding map GenLoop.toSphere p : Sⁿ → X is freely homotopic to a constant map.

theorem HomotopyGroup.mk_eq_one_iff_nullhomotopic_diskBoundaryMap {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} (p : ↑(GenLoop (Fin n) (↑X) x)) : ⟦p⟧ = 1 ↔ (TopCat.Hom.hom (GenLoop.diskBoundaryMap p)).Nullhomotopic

A homotopy class is trivial exactly when its attaching map is null-homotopic. The class of a generalized loop p is the identity of πₙ(X, x) if and only if the map GenLoop.diskBoundaryMap p : ∂𝔻 (n + 1) ⟶ X, along which a cell kills that class, is freely null-homotopic.

theorem HomotopyGroup.map_mk_eq_one_iff_nullhomotopic_diskBoundaryMap_comp {n : ℕ} [NeZero n] {X Y : TopCat} {x : ↑X} {y : ↑Y} (f : X ⟶ Y) (hf : (CategoryTheory.ConcreteCategory.hom f) x = y) (p : ↑(GenLoop (Fin n) (↑X) x)) : map (TopCat.Hom.hom f) hf ⟦p⟧ = 1 ↔ (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (GenLoop.diskBoundaryMap p) f)).Nullhomotopic

A based map kills a class exactly when it extends the attaching map over a disk. The image of the class of p under a based map f is the identity exactly when the attaching map GenLoop.diskBoundaryMap p followed by f is null-homotopic.