# Documentation

Mathlib.Topology.Homotopy.HomotopyGroup

# 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).
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.

Instances For
@[reducible]
def Cube.splitAt {N : Type u_1} [] (i : N) :
(N) ≃ₜ × ({ j // j i })

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

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

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

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

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

Instances For
Instances For
instance LoopSpace.inhabited (X : Type u_2) [] (x : X) :
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.

Instances For
Instances For
instance GenLoop.funLike {N : Type u_1} {X : Type u_2} [] {x : X} :
FunLike (↑(GenLoop N X x)) (N) fun x => X
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) :
{ val := f, property := 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.

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.

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

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)
@[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) = ↑() t
def GenLoop.toLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : ↑(GenLoop N X x)) :
LoopSpace (↑(GenLoop { j // j i } X x)) GenLoop.const

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

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 // j i } X x)) GenLoop.const) :
def GenLoop.fromLoop {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace (↑(GenLoop { j // 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$.

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 // j i } X x)) GenLoop.const) :
= p
@[simp]
theorem GenLoop.loopHomeo_symm_apply {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) (p : LoopSpace (↑(GenLoop { j // 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 =
def GenLoop.loopHomeo {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
↑(GenLoop N X x) ≃ₜ LoopSpace (↑(GenLoop { j // 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.

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 // 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 // j i } X x)) GenLoop.const} {t : N} :
↑() t = ↑(p (t i)) (↑() t).snd
@[reducible]
def GenLoop.cCompInsert {N : Type u_1} {X : Type u_2} [] [] (i : N) :
C(C(N, X), C( × ({ j // j i }), X))

Composition with Cube.insertAt as a continuous map.

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 : ContinuousMap.HomotopyRel (p) (q) ()) :
C(, C({ j // 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.

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 : ContinuousMap.HomotopyRel (p) (q) ()) (t : ) (tₙ : { j // j i }) :
↑(↑() t) tₙ = H (t.fst, ↑() (t.snd, 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.fst, Prod.snd a i)) fun j => Prod.snd a 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.

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.

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.

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.

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

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

Instances For
@[reducible]
def HomotopyGroup.Pi (n : ) (X : Type u_3) [] (x : X) :
Type u_3

Homotopy group of finite index.

Instances For
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.

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.

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

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

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.

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.

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

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

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

@[reducible]
def 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.

Instances For
theorem HomotopyGroup.isUnital_auxGroup {N : Type u_1} {X : Type u_2} [] {x : X} [] (i : N) :
EckmannHilton.IsUnital Mul.mul (Quotient.mk () 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 = Quotient.mk () 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 x_1 => x * x_1) () () = Quotient.mk () ()

Characterization of multiplication

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

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.