The homotopy-group shift for Moore loops

Normalizing a Moore loop to the unit interval induces the usual loop-space shift on higher homotopy groups. This identifies πₖ(ΩᴹX, 1) with πₖ₊₁(X, x) for positive k, identifies the path components of the double Moore loop space with the elements of π₂(X, x) (TauCeti.MooreLoopSpace.zerothHomotopyDoubleEquiv), and shows that the double Moore loop space is path connected when π₂(X, x) vanishes.

The unit is not special: concatenation in front with a Moore loop γ is a homotopy equivalence of the Moore loop space carrying the unit to γ, so the positive homotopy groups of ΩᴹX at γ vanish exactly when the corresponding higher homotopy groups of X do (TauCeti.MooreLoopSpace.subsingleton_homotopyGroup_succ_iff). In particular every path component of the Moore loop space of an aspherical space is weakly contractible.

The comparison uses the specified Moore/fixed-interval homotopy equivalence. The basepoint is the Moore loop of duration zero, which normalizes to the constant fixed-interval loop.

• A. Hatcher, Algebraic Topology, §4.1.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter I.

noncomputable def TauCeti.MooreLoopSpace.homotopyGroupMulEquiv {X : Type u_1} [TopologicalSpace X] (x : X) (n : ℕ) : HomotopyGroup.Pi (n + 1) (MooreLoopSpace X x) 1 ≃* HomotopyGroup.Pi (n + 2) X x

The positive homotopy groups of Moore loops are the higher homotopy groups of the original space, via normalization to the unit interval and the loop-space shift.

@[simp]

theorem TauCeti.MooreLoopSpace.homotopyGroupMulEquiv_apply {X : Type u_1} [TopologicalSpace X] (x : X) (n : ℕ) (a : HomotopyGroup.Pi (n + 1) (MooreLoopSpace X x) 1) : (homotopyGroupMulEquiv x n) a = (HomotopyGroup.pathLoopSpaceMulEquiv n) (HomotopyGroup.map (homotopyEquivPath x).toFun ⋯ a)

The Moore loop-space shift applies the map induced by normalization and then the fixed-interval loop-space shift.

noncomputable def TauCeti.MooreLoopSpace.zerothHomotopyDoubleEquiv {X : Type u_1} [TopologicalSpace X] (x : X) : ZerothHomotopy (MooreLoopSpace (MooreLoopSpace X x) 1) ≃ HomotopyGroup.Pi 2 X x

The path components of the double Moore loop space are the second homotopy group.

@[simp]

theorem TauCeti.MooreLoopSpace.zerothHomotopyDoubleEquiv_mk {X : Type u_1} [TopologicalSpace X] (x : X) (γ : MooreLoopSpace (MooreLoopSpace X x) 1) : (zerothHomotopyDoubleEquiv x) (ZerothHomotopy.mk γ) = (homotopyGroupMulEquiv x 0) (HomotopyGroup.pi1MulEquivFundamentalGroup.symm ((fundamentalGroupHom 1) γ))

The component of a double Moore loop γ is the image of its class in the fundamental group of ΩᴹX under the Moore loop-space shift.

@[simp]

theorem TauCeti.MooreLoopSpace.zerothHomotopyDoubleEquiv_mk_one {X : Type u_1} [TopologicalSpace X] (x : X) : (zerothHomotopyDoubleEquiv x) (ZerothHomotopy.mk 1) = 1

The component of the constant double Moore loop is the identity of π₂(X, x).

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_iff_subsingleton_pi1 {X : Type u_1} [TopologicalSpace X] (x : X) : PathConnectedSpace (MooreLoopSpace X x) ↔ Subsingleton (HomotopyGroup.Pi 1 X x)

The Moore loop space MooreLoopSpace X x is path connected if and only if π_ 1 X x is trivial.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_double_iff {X : Type u_1} [TopologicalSpace X] (x : X) : PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1) ↔ Subsingleton (HomotopyGroup.Pi 2 X x)

The double Moore loop space MooreLoopSpace (MooreLoopSpace X x) 1 is path connected if and only if π_ 2 X x is trivial.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_double {X : Type u_1} [TopologicalSpace X] (x : X) [Subsingleton (HomotopyGroup.Pi 2 X x)] : PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1)

The double Moore loop space is path connected when the second homotopy group of the original space vanishes.

theorem TauCeti.MooreLoopSpace.subsingleton_homotopyGroup_iff {X : Type u_1} [TopologicalSpace X] (x : X) (k : ℕ) : Subsingleton (HomotopyGroup.Pi k (MooreLoopSpace X x) 1) ↔ Subsingleton (HomotopyGroup.Pi (k + 1) X x)

The homotopy group π_ k (MooreLoopSpace X x) 1 (including k = 0) is trivial if and only if π_ (k + 1) X x is trivial.

theorem TauCeti.MooreLoopSpace.forall_subsingleton_homotopyGroup_iff {X : Type u_1} [TopologicalSpace X] (x : X) : (∀ (k : ℕ), Subsingleton (HomotopyGroup.Pi k (MooreLoopSpace X x) 1)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)

All homotopy groups π_ k (MooreLoopSpace X x) 1 (including k = 0) are trivial if and only if π_ (n + 1) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.forall_subsingleton_homotopyGroup_double_iff {X : Type u_1} [TopologicalSpace X] (x : X) : (∀ (k : ℕ), Subsingleton (HomotopyGroup.Pi k (MooreLoopSpace (MooreLoopSpace X x) 1) 1)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

All homotopy groups of the double Moore loop space MooreLoopSpace (MooreLoopSpace X x) 1 (including k = 0) are trivial if and only if π_ (n + 2) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.subsingleton_homotopyGroup_succ_iff {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) (n : ℕ) : Subsingleton (HomotopyGroup.Pi (n + 1) (MooreLoopSpace X x) γ) ↔ Subsingleton (HomotopyGroup.Pi (n + 2) X x)

At every Moore loop γ, not only at the unit, the homotopy group π_ (n + 1) of the Moore loop space is trivial exactly when π_ (n + 2) X x is. Concatenation in front with γ is a homotopy equivalence of the Moore loop space, with homotopy inverse concatenation in front with the reversal of γ, and it carries the unit to γ.