# nth homotopy group #

We define the nth 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 functions I^N → X that send the boundary to x,
• HomotopyGroup.Pi n X x denoted π_ n X x is the quotient of GenLoop (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 when M ≃ N. Similarly for π_.
• Path-induced homomorphisms. Show that HomotopyGroup.pi1EquivFundamentalGroup is a group isomorphism.
• Examples with 𝕊^n: π_n (𝕊^n) = ℤ, π_m (𝕊^n) trivial for m < n.
• Actions of π_1 on π_n.
• Lie algebra: ⁅π_(n+1), π_(m+1)⁆ contained in π_(n+m+1).
Equations
Instances For
def Cube.boundary (N : Type u_1) :
Set (N)

The points in a cube with at least one projection equal to 0 or 1.

Equations
• = {y : N | ∃ (i : N), y i = 0 y i = 1}
Instances For
@[reducible, inline]
abbrev Cube.splitAt {N : Type u_1} [] (i : N) :
(N) ≃ₜ × ({ j : N // j i })

The forward direction of the homeomorphism between the cube $I^N$ and $I × I^{N\setminus{j}}$.

Equations
Instances For
@[reducible, inline]
abbrev Cube.insertAt {N : Type u_1} [] (i : N) :
× ({ j : N // j i }) ≃ₜ (N)

The backward direction of the homeomorphism between the cube $I^N$ and $I × I^{N\setminus{j}}$.

Equations
• = .symm
Instances For
theorem Cube.insertAt_boundary {N : Type u_1} [] (i : N) {t₀ : } {t : { j : N // j i }} (H : (t₀ = 0 t₀ = 1) t Cube.boundary { j : N // j i }) :
() (t₀, t)
@[reducible, inline]
abbrev LoopSpace (X : Type u_2) [] (x : X) :
Type u_2

The space of paths with both endpoints equal to a specified point x : X.

Equations
Instances For
Equations
Instances For
instance LoopSpace.inhabited (X : Type u_2) [] (x : X) :
Equations
• = { default := }
def GenLoop (N : Type u_1) (X : Type u_2) [] (x : X) :
Set C(N, X)

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.

Equations
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.

Equations
Instances For
instance GenLoop.instFunLike {N : Type u_1} {X : Type u_2} [] {x : X} :
FunLike ((GenLoop N X x)) (N) X
Equations
• GenLoop.instFunLike = { coe := fun (f : (GenLoop N X x)) => f, coe_injective' := }
theorem GenLoop.ext {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) (g : (GenLoop N X x)) (H : ∀ (y : N), f y = g y) :
f = g
@[simp]
theorem GenLoop.mk_apply {N : Type u_1} {X : Type u_2} [] {x : X} (f : C(N, X)) (H : f GenLoop N X x) (y : N) :
f, H y = f y
def GenLoop.copy {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) (g : (N)X) (h : g = f) :
(GenLoop N X x)

Copy of a GenLoop with a new map from the unit cube equal to the old one. Useful to fix definitional equalities.

Equations
• GenLoop.copy f g h = { toFun := g, continuous_toFun := },
Instances For
theorem GenLoop.coe_copy {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) {g : (N)X} (h : g = f) :
(GenLoop.copy f g h) = g
theorem GenLoop.copy_eq {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) {g : (N)X} (h : g = f) :
GenLoop.copy f g h = f
theorem GenLoop.boundary {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) (y : N) :
f y = x
def GenLoop.const {N : Type u_1} {X : Type u_2} [] {x : X} :
(GenLoop N X x)

The constant GenLoop at x.

Equations
Instances For
@[simp]
theorem GenLoop.const_apply {N : Type u_1} {X : Type u_2} [] {x : X} {t : N} :
GenLoop.const t = x
instance GenLoop.inhabited {N : Type u_1} {X : Type u_2} [] {x : X} :
Inhabited (GenLoop N X x)
Equations
• GenLoop.inhabited = { default := GenLoop.const }
def GenLoop.Homotopic {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) (g : (GenLoop N X x)) :

The "homotopic relative to boundary" relation between GenLoops.

Equations
• = (f).HomotopicRel (g) ()
Instances For
theorem GenLoop.Homotopic.refl {N : Type u_1} {X : Type u_2} [] {x : X} (f : (GenLoop N X x)) :
theorem GenLoop.Homotopic.symm {N : Type u_1} {X : Type u_2} [] {x : X} {f : (GenLoop N X x)} {g : (GenLoop N X x)} (H : ) :
theorem GenLoop.Homotopic.trans {N : Type u_1} {X : Type u_2} [] {x : X} {f : (GenLoop N X x)} {g : (GenLoop N X x)} {h : (GenLoop N X x)} (H0 : ) (H1 : ) :
theorem GenLoop.Homotopic.equiv {N : Type u_1} {X : Type u_2} [] {x : X} :
Equivalence GenLoop.Homotopic
instance GenLoop.Homotopic.setoid {X : Type u_2} [] (N : Type u_3) (x : X) :
Setoid (GenLoop N X x)
Equations
• = { r := GenLoop.Homotopic, iseqv := }
@[simp]
theorem GenLoop.toLoop_apply_coe {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : (GenLoop N X x)) (t : ) :
(() t) = ((p).comp ().toContinuousMap).curry t
def GenLoop.toLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : (GenLoop N X x)) :
LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const

Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus{j}} → X)$.

Equations
• = { toFun := fun (t : ) => ((p).comp ().toContinuousMap).curry t, , continuous_toFun := , source' := , target' := }
Instances For
theorem GenLoop.continuous_toLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
@[simp]
theorem GenLoop.fromLoop_coe {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const) :
() = ({ toFun := Subtype.val, continuous_toFun := }.comp p.toContinuousMap).uncurry.comp ().toContinuousMap
def GenLoop.fromLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const) :
(GenLoop N X x)

Generalized loop from a loop by uncurrying $I → (I^{N\setminus{j}} → X)$ into $I^N → X$.

Equations
• = ({ toFun := Subtype.val, continuous_toFun := }.comp p.toContinuousMap).uncurry.comp ().toContinuousMap,
Instances For
theorem GenLoop.continuous_fromLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
theorem GenLoop.to_from {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const) :
= p
@[simp]
theorem GenLoop.loopHomeo_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : (GenLoop N X x)) :
p =
@[simp]
theorem GenLoop.loopHomeo_symm_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const) :
.symm p =
def GenLoop.loopHomeo {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
(GenLoop N X x) ≃ₜ LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const

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.

Equations
• = { toFun := , invFun := , left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
Instances For
theorem GenLoop.toLoop_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {t : } {tn : { j : N // j i }} :
(() t) tn = p (() (t, tn))
theorem GenLoop.fromLoop_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : LoopSpace ((GenLoop { j : N // j i } X x)) GenLoop.const} {t : N} :
() t = (p (t i)) (() t).2
@[reducible, inline]
abbrev GenLoop.cCompInsert {N : Type u_1} {X : Type u_2} [] [] (i : N) :
C(C(N, X), C( × ({ j : N // j i }), X))

Composition with Cube.insertAt as a continuous map.

Equations
• = { toFun := fun (f : C(N, X)) => f.comp ().toContinuousMap, continuous_toFun := }
Instances For
def GenLoop.homotopyTo {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : (p).HomotopyRel (q) ()) :
C(, C({ j : N // j i }, X))

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.

Equations
• = ({ toFun := ContinuousMap.curry, continuous_toFun := }.comp (.comp H.curry)).uncurry
Instances For
theorem GenLoop.homotopyTo_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : (p).HomotopyRel (q) ()) (t : ) (tₙ : { j : N // j i }) :
(() t) tₙ = H (t.1, () (t.2, tₙ))
theorem GenLoop.homotopicTo {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
Path.Homotopic () ()
@[simp]
theorem GenLoop.homotopyFrom_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : Path.Homotopy () ()) :
∀ (a : × (N)), () a = (H (a.1, a.2 i)) fun (j : { j : N // ¬j = i }) => a.2 j
def GenLoop.homotopyFrom {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : Path.Homotopy () ()) :
C( × (N), X)

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem GenLoop.homotopicFrom {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
Path.Homotopic () ()
def GenLoop.transAt {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (f : (GenLoop N X x)) (g : (GenLoop N X x)) :
(GenLoop N X x)

Concatenation of two GenLoops along the ith coordinate.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def GenLoop.symmAt {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (f : (GenLoop N X x)) :
(GenLoop N X x)

Reversal of a GenLoop along the ith coordinate.

Equations
Instances For
theorem GenLoop.transAt_distrib {N : Type u_1} {X : Type u_2} [] {x : X} [] {i : N} {j : N} (h : i j) (a : (GenLoop N X x)) (b : (GenLoop N X x)) (c : (GenLoop N X x)) (d : (GenLoop N X x)) :
theorem GenLoop.fromLoop_trans_toLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] {i : N} {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
theorem GenLoop.fromLoop_symm_toLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] {i : N} {p : (GenLoop N X x)} :
def HomotopyGroup (N : Type u_3) (X : Type u_4) [] (x : X) :
Type (max u_3 u_4)

The nth homotopy group at x defined as the quotient of Ω^n x by the GenLoop.Homotopic relation.

Equations
Instances For
instance instInhabitedHomotopyGroup {N : Type u_1} {X : Type u_2} [] {x : X} :
Equations
• instInhabitedHomotopyGroup =
def homotopyGroupEquivFundamentalGroup {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
FundamentalGroup ((GenLoop { j : N // j i } X x)) GenLoop.const

Equivalence between the homotopy group of X and the fundamental group of Ω^{j // j ≠ i} x.

Equations
Instances For
@[reducible, inline]
abbrev HomotopyGroup.Pi (n : ) (X : Type u_3) [] (x : X) :
Type u_3

Homotopy group of finite index.

Equations
Instances For
Equations
Instances For
def genLoopHomeoOfIsEmpty {X : Type u_2} [] (N : Type u_3) (x : X) [] :
(GenLoop N X x) ≃ₜ X

The 0-dimensional generalized loops based at x are in bijection with X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def homotopyGroupEquivZerothHomotopyOfIsEmpty {X : Type u_2} [] (N : Type u_3) (x : X) [] :

The homotopy "group" indexed by an empty type is in bijection with the path components of X, aka the ZerothHomotopy.

Equations
Instances For
def HomotopyGroup.pi0EquivZerothHomotopy {X : Type u_2} [] {x : X} :

The 0th homotopy "group" is in bijection with ZerothHomotopy.

Equations
• HomotopyGroup.pi0EquivZerothHomotopy =
Instances For
def genLoopEquivOfUnique {X : Type u_2} [] {x : X} (N : Type u_3) [] :
(GenLoop N X x)

The 1-dimensional generalized loops based at x are in bijection with loops at x.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def homotopyGroupEquivFundamentalGroupOfUnique {X : Type u_2} [] {x : X} (N : Type u_3) [] :

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.

Equations
Instances For
def HomotopyGroup.pi1EquivFundamentalGroup {X : Type u_2} [] {x : X} :

The first homotopy group at x is in bijection with the fundamental group.

Equations
• HomotopyGroup.pi1EquivFundamentalGroup =
Instances For
instance HomotopyGroup.group {X : Type u_2} [] {x : X} (N : Type u_3) [] [] :

Group structure on HomotopyGroup N X x for nonempty N (in particular π_(n+1) X x).

Equations
@[reducible, inline]
abbrev HomotopyGroup.auxGroup {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :

Group structure on HomotopyGroup obtained by pulling back path composition along the ith direction. The group structures for two different i j : N distribute over each other, and therefore are equal by the Eckmann-Hilton argument.

Equations
Instances For
theorem HomotopyGroup.isUnital_auxGroup {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
EckmannHilton.IsUnital Mul.mul GenLoop.const
theorem HomotopyGroup.auxGroup_indep {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (j : N) :
theorem HomotopyGroup.transAt_indep {N : Type u_1} {X : Type u_2} [] {x : X} [] {i : N} (j : N) (f : (GenLoop N X x)) (g : (GenLoop N X x)) :
=
theorem HomotopyGroup.symmAt_indep {N : Type u_1} {X : Type u_2} [] {x : X} [] {i : N} (j : N) (f : (GenLoop N X x)) :
=
theorem HomotopyGroup.one_def {N : Type u_1} {X : Type u_2} [] {x : X} [] [] :
1 = GenLoop.const

Characterization of multiplicative identity

theorem HomotopyGroup.mul_spec {N : Type u_1} {X : Type u_2} [] {x : X} [] [] {i : N} {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
(fun (x_1 x_2 : ) => x_1 * x_2) p q =

Characterization of multiplication

theorem HomotopyGroup.inv_spec {N : Type u_1} {X : Type u_2} [] {x : X} [] [] {i : N} {p : (GenLoop N X x)} :
(p)⁻¹ =

Characterization of multiplicative inverse

instance HomotopyGroup.commGroup {N : Type u_1} {X : Type u_2} [] {x : X} [] [] :

Multiplication on HomotopyGroup N X x is commutative for nontrivial N. In particular, multiplication on π_(n+2) is commutative.

Equations
• HomotopyGroup.commGroup = let h := ;