n
th homotopy group #
We define the n
th homotopy group at x : X
, π_n X x
, as the equivalence classes
of functions from the n
-dimensional cube to the topological space X
that send the boundary to the base point x
, up to homotopic equivalence.
Note that such functions are generalized loops GenLoop (Fin n) x
; in particular
GenLoop (Fin 1) x ≃ Path x x
.
We show that π_0 X x
is equivalent to the path-connected components, and
that π_1 X x
is equivalent to the fundamental group at x
.
We provide a group instance using path composition and show commutativity when n > 1
.
definitions #
GenLoop N x
is the type of continuous functionsI^N → X
that send the boundary tox
,HomotopyGroup.Pi n X x
denotedπ_ n X x
is the quotient ofGenLoop (Fin n) x
by homotopy relative to the boundary,- group instance
Group (π_(n+1) X x)
, - commutative group instance
CommGroup (π_(n+2) X x)
.
TODO:
Ω^M (Ω^N X) ≃ₜ Ω^(M⊕N) X
, andΩ^M X ≃ₜ Ω^N X
whenM ≃ N
. Similarly forπ_
.- Path-induced homomorphisms. Show that
HomotopyGroup.pi1EquivFundamentalGroup
is a group isomorphism. - Examples with
𝕊^n
:π_n (𝕊^n) = ℤ
,π_m (𝕊^n)
trivial form < n
. - Actions of π_1 on π_n.
- Lie algebra:
⁅π_(n+1), π_(m+1)⁆
contained inπ_(n+m+1)
.
The points in a cube with at least one projection equal to 0 or 1.
Instances For
The forward direction of the homeomorphism between the cube $I^N$ and $I × I^{N\setminus{j}}$.
Instances For
The backward direction of the homeomorphism between the cube $I^N$ and $I × I^{N\setminus{j}}$.
Instances For
The space of paths with both endpoints equal to a specified point x : X
.
Instances For
The n
-dimensional generalized loops based at x
in a space X
are
continuous functions I^n → X
that sends the boundary to x
.
We allow an arbitrary indexing type N
in place of Fin n
here.
Instances For
Copy of a GenLoop
with a new map from the unit cube equal to the old one.
Useful to fix definitional equalities.
Instances For
The constant GenLoop
at x
.
Instances For
The "homotopic relative to boundary" relation between GenLoop
s.
Instances For
Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus{j}} → X)$.
Instances For
Generalized loop from a loop by uncurrying $I → (I^{N\setminus{j}} → X)$ into $I^N → X$.
Instances For
The n+1
-dimensional loops are in bijection with the loops in the space of
n
-dimensional loops with base point const
.
We allow an arbitrary indexing type N
in place of Fin n
here.
Instances For
Composition with Cube.insertAt
as a continuous map.
Instances For
A homotopy between n+1
-dimensional loops p
and q
constant on the boundary
seen as a homotopy between two paths in the space of n
-dimensional paths.
Instances For
The converse to GenLoop.homotopyTo
: a homotopy between two loops in the space of
n
-dimensional loops can be seen as a homotopy between two n+1
-dimensional paths.
Instances For
Concatenation of two GenLoop
s along the i
th coordinate.
Instances For
Reversal of a GenLoop
along the i
th coordinate.
Instances For
The n
th homotopy group at x
defined as the quotient of Ω^n x
by the
GenLoop.Homotopic
relation.
Instances For
Equivalence between the homotopy group of X and the fundamental group of
Ω^{j // j ≠ i} x
.
Instances For
Homotopy group of finite index.
Instances For
The 0-dimensional generalized loops based at x
are in bijection with X
.
Instances For
The homotopy "group" indexed by an empty type is in bijection with
the path components of X
, aka the ZerothHomotopy
.
Instances For
The 0th homotopy "group" is in bijection with ZerothHomotopy
.
Instances For
The 1-dimensional generalized loops based at x
are in bijection with loops at x
.
Instances For
The homotopy group at x
indexed by a singleton is in bijection with the fundamental group,
i.e. the loops based at x
up to homotopy.
Instances For
The first homotopy group at x
is in bijection with the fundamental group.
Instances For
Group structure on HomotopyGroup N X x
for nonempty N
(in particular π_(n+1) X x
).
Group structure on HomotopyGroup
obtained by pulling back path composition along the
i
th direction. The group structures for two different i j : N
distribute over each
other, and therefore are equal by the Eckmann-Hilton argument.
Instances For
Characterization of multiplicative identity
Characterization of multiplication
Characterization of multiplicative inverse
Multiplication on HomotopyGroup N X x
is commutative for nontrivial N
.
In particular, multiplication on π_(n+2)
is commutative.