The loop-space shift for higher homotopy groups #
GenLoop.homotopic_iff_joined identifies homotopy of generalized loops relative to the cube
boundary with path connectedness in Ω^ N X x. The payoff, proved here, is that any
homeomorphism between generalized-loop spaces preserves and reflects homotopy, hence descends to
a bijection of homotopy groups. Two of Mathlib's homeomorphisms are then put to work.
GenLoop.congr, reindexing the cube along an equivalenceM ≃ Nof index types, givesHomotopyGroup.congrEquivand its multiplicative form.GenLoop.genLoopGenLoopEquiv : Ω^ M (Ω^ N X x) const ≃ₜ Ω^ (M ⊕ N) X x, currying a cube inM ⊕ Ndirections into anM-cube ofN-cubes, gives the loop-space shiftπ_M (Ω^ N X x) ≃* π_(M ⊕ N) X x. Specialised toNa singleton and Mathlib's loop spaceΩ X x = Path x x, this is the classicalπ_(n + 1)(Ω X) ≅ π_(n + 2)(X).
Read on the quotient instead of on representatives, the same correspondence is a statement
about path components: HomotopyGroup N X x is the set of path components of Ω^ N X x. For
N a singleton this says that two loops at x are joined in Ω X x exactly when they are
homotopic, so the path components of Ω X x are the fundamental group of X at x.
Multiplicativity is checked by hand in both cases: the product on HomotopyGroup N X x is
computed by HomotopyGroup.mul_spec as the class of a concatenation GenLoop.transAt i in an
arbitrary cube direction i, and both homeomorphisms carry a concatenation in direction i to a
concatenation in the matching direction.
Main declarations #
Homeomorph.genLoopHomotopic_iff: a homeomorphism of generalized-loop spaces preserves and reflects homotopy.HomotopyGroup.congrEquiv,HomotopyGroup.congrMulEquiv: reindexing the cube directions alongM ≃ N, natural in the space byHomotopyGroup.map_congrEquivandHomotopyGroup.map_eq_congrEquiv_symm_comp.HomotopyGroup.zerothHomotopyEquiv:π_N(X, x)is the set of path components ofΩ^ N X x, withPath.joined_iff_homotopicits one-dimensional form andHomotopyGroup.zerothHomotopyLoopSpaceEquivFundamentalGroupthe degree-zero shiftπ_0(Ω X) ≅ π_1(X).HomotopyGroup.loopSpaceEquiv,HomotopyGroup.loopSpaceMulEquiv: the loop-space shiftπ_M (Ω^ N X x) const ≃* π_(M ⊕ N) X x.HomotopyGroup.piLoopSpaceMulEquiv,HomotopyGroup.pathLoopSpaceMulEquiv: itsπ_nforms, the latter for Mathlib's loop spaceΩ X x.HomotopyGroup.fundamentalGroupLoopSpaceMulEquiv: its degree-one formπ₁(Ω X x, refl x) ≃* π₂(X, x), with the fundamental group of the loop space.TauCeti.zerothHomotopyDoubleLoopSpaceEquiv: the path components of the double loop spaceΩ (Ω X x) (Path.refl x)are the elements ofπ₂(X, x).
References #
The loop-space shift is the cubical form of the standard isomorphism
π_n(Ω X) ≅ π_(n + 1)(X); see Hatcher, Algebraic Topology, Section 4.1.
Reindexing the cube directions #
An equivalence M ≃ N of index types reindexes the cube directions, and so identifies the
homotopy groups indexed by M and by N.
Instances For
Reindexing the cube directions commutes with the maps induced by based continuous maps.
The map induced on the homotopy group indexed by M is the map induced on the group indexed
by N, conjugated by the reindexing e : M ≃ N of the cube directions.
Reindexing the cube directions along e : M ≃ N does not change whether a based map induces
a bijection on homotopy groups.
In positive dimensions, reindexing the cube directions along e : M ≃ N is an isomorphism
of homotopy groups. The target index type inherits its nonemptiness, hence its group structure,
from e; that is what the letI in the statement records.
Instances For
In positive dimensions, reindexing the cube directions commutes with the maps induced by based continuous maps.
Homotopy groups as path components of the loop space #
The homotopy group π_N(X, x) is the set of path components of the space of
N-dimensional generalized loops. This is GenLoop.homotopic_iff_joined read on the
quotient.
Instances For
Mathlib's homeomorphism Ω^ N X x ≃ₜ X for empty N evaluates a zero-dimensional
generalized loop at the unique point of the cube.
The inverse of Mathlib's homeomorphism Ω^ N X x ≃ₜ X for empty N sends a point to the
constant zero-dimensional generalized loop at it.
Mathlib's bijection between the homotopy group indexed by an empty type and the path
components of X sends the class of a zero-dimensional generalized loop to the path component of
its value.
The image under a based map of the class of a zero-dimensional generalized loop is the path component of the image of its value.
Classes of zero-dimensional generalized loops are path components. Two such loops have the same class exactly when their values are joined by a path.
Two loops at x are joined by a path in the loop space exactly when they are homotopic.
This is GenLoop.homotopic_iff_joined for a singleton index type, carried across the
homeomorphism GenLoop.homeomorphOfUnique onto Mathlib's loop space Ω X x.
The path components of Mathlib's loop space Ω X x are the fundamental group of X
at x: the degree-zero case of the loop-space shift. Both sides are quotients of Ω X x, by
path connectedness and by homotopy respectively, and Path.joined_iff_homotopic says the two
relations agree.
Instances For
The loop-space shift #
The loop-space shift. Currying identifies the homotopy group indexed by M of the space
of N-dimensional generalized loops, based at the constant loop, with the homotopy group of X
indexed by M ⊕ N.
Instances For
The loop-space shift is an isomorphism of groups in positive dimensions:
π_M (Ω^ N X x) ≃* π_(M ⊕ N) X x.
Instances For
The loop-space shift in the π_n notation: π_(m + 1) of the space of n-dimensional
generalized loops is π_(m + 1 + n) of the space itself.
Instances For
The homotopy groups of the loop space are the higher homotopy groups of the space:
π_(m + 1)(Ω X, refl x) ≃* π_(m + 2)(X, x).
Instances For
The fundamental group of the loop space is the second homotopy group:
π₁(Ω X x, refl x) ≃* π₂(X, x), the case m = 0 of pathLoopSpaceMulEquiv read through
pi1MulEquivFundamentalGroup. A loop of loops s ↦ γ_s at the constant loop is the square
(s, t) ↦ γ_s t, which sends the boundary of the square to x.
Instances For
The shift loopSpaceEquiv is natural: it commutes with the maps induced on homotopy sets by a
based map f and by any map F of cube-loop spaces that postcomposes with f.
The π_n form of the shift is natural, for any map F of cube-loop spaces that postcomposes
with f.
The shift pathLoopSpaceMulEquiv is natural: it commutes with the maps induced on homotopy
groups by a based map f and by any map F of loop spaces that postcomposes loops with f.
The fixed-interval loop space Ω X x is path connected if and only if the fundamental group
FundamentalGroup X x is trivial.
The fixed-interval loop space Ω X x is path connected if and only if π_ 1 X x is trivial.
The fixed-interval double loop space Ω (Ω X x) (Path.refl x) is path connected if and only if
π_ 2 X x is trivial.
The homotopy group π_ k (Ω X x) (Path.refl x) (including k = 0) is trivial if and only if
π_ (k + 1) X x is trivial.
All homotopy groups π_ k (Ω X x) (Path.refl x) (including k = 0) are trivial if and only if
π_ (n + 1) X x is trivial for every n : ℕ.
All homotopy groups of the fixed-interval double loop space Ω (Ω X x) (Path.refl x)
(including k = 0) are trivial if and only if π_ (n + 2) X x is trivial for every n : ℕ.
The path components of the double loop space are the second homotopy group. The
component of a double loop γ is sent to the class of γ under the loop-space shift.
Instances For
The component of a double loop γ is the image of its homotopy class under
fundamentalGroupLoopSpaceMulEquiv.
The component of the constant double loop is the identity of π₂(X, x).