# mathlib3documentation

topology.homotopy.homotopy_group

# nth homotopy group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 gen_loop (fin n) x; in particular gen_loop (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 #

• gen_loop N x is the type of continuous fuctions I^N → X that send the boundary to x,
• homotopy_group.pi n X x denoted π_ n X x is the quotient of gen_loop (fin n) x by homotopy relative to the boundary,
• group instance group (π_(n+1) X x),
• commutative group instance comm_group (π_(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 homotopy_group.pi_1_equiv_fundamental_group 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).
def cube.boundary (N : Type u_1) :

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

Equations
@[reducible]
def cube.split_at {N : Type u_1} [decidable_eq N] (i : N) :

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

Equations
@[reducible]
def cube.insert_at {N : Type u_1} [decidable_eq N] (i : N) :

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

Equations
theorem cube.insert_at_boundary {N : Type u_1} [decidable_eq N] (i : N) {t₀ : unit_interval} {t : {j // j i} unit_interval} (H : (t₀ = 0 t₀ = 1) t cube.boundary {j // j i}) :
(t₀, t)
@[reducible]
def loop_space (X : Type u_2) (x : X) :
Type u_2

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

Equations
@[protected, instance]
def loop_space.inhabited (X : Type u_2) (x : X) :
Equations
def gen_loop (N : Type u_1) (X : Type u_2) (x : 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 ↥gen_loop
def gen_loop.copy {N : Type u_1} {X : Type u_2} {x : X} (f : (gen_loop N X x)) (g : X) (h : g = f) :
(gen_loop N X x)

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

Equations
theorem gen_loop.coe_copy {N : Type u_1} {X : Type u_2} {x : X} (f : (gen_loop N X x)) {g : X} (h : g = f) :
g h) = g
theorem gen_loop.copy_eq {N : Type u_1} {X : Type u_2} {x : X} (f : (gen_loop N X x)) {g : X} (h : g = f) :
h = f
theorem gen_loop.boundary {N : Type u_1} {X : Type u_2} {x : X} (f : (gen_loop N X x)) (y : N unit_interval) (H : y ) :
f y = x
@[protected, instance]
def gen_loop.fun_like {N : Type u_1} {X : Type u_2} {x : X} :
fun_like (gen_loop N X x) (λ (_x : , X)
Equations
@[ext]
theorem gen_loop.ext {N : Type u_1} {X : Type u_2} {x : X} (f g : (gen_loop N X x)) (H : (y : , f y = g y) :
f = g
@[simp]
theorem gen_loop.mk_apply {N : Type u_1} {X : Type u_2} {x : X} (f : C(, X)) (H : f X x) (y : N unit_interval) :
f, H⟩ y = f y
def gen_loop.const {N : Type u_1} {X : Type u_2} {x : X} :
(gen_loop N X x)

The constant gen_loop at x.

Equations
@[simp]
theorem gen_loop.const_apply {N : Type u_1} {X : Type u_2} {x : X} {t : N unit_interval} :
@[protected, instance]
def gen_loop.inhabited {N : Type u_1} {X : Type u_2} {x : X} :
Equations
def gen_loop.homotopic {N : Type u_1} {X : Type u_2} {x : X} (f g : (gen_loop N X x)) :
Prop

The "homotopic relative to boundary" relation between gen_loops.

Equations
@[refl]
theorem gen_loop.homotopic.refl {N : Type u_1} {X : Type u_2} {x : X} (f : (gen_loop N X x)) :
@[symm]
theorem gen_loop.homotopic.symm {N : Type u_1} {X : Type u_2} {x : X} {f g : (gen_loop N X x)} (H : g) :
@[trans]
theorem gen_loop.homotopic.trans {N : Type u_1} {X : Type u_2} {x : X} {f g h : (gen_loop N X x)} (H0 : g) (H1 : h) :
theorem gen_loop.homotopic.equiv {N : Type u_1} {X : Type u_2} {x : X} :
@[protected, instance]
def gen_loop.homotopic.setoid {X : Type u_2} (N : Type u_1) (x : X) :
Equations
def gen_loop.to_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : (gen_loop N X x)) :

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

Equations
@[simp]
theorem gen_loop.to_loop_apply_coe {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : (gen_loop N X x)) (t : unit_interval) :
( p) t) = ((p.val.comp .curry) t
theorem gen_loop.continuous_to_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :
def gen_loop.from_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
(gen_loop N X x)

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

Equations
@[simp]
theorem gen_loop.from_loop_coe {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
theorem gen_loop.continuous_from_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :
theorem gen_loop.to_from {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
= p
def gen_loop.loop_homeo {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :

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
@[simp]
theorem gen_loop.loop_homeo_symm_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
.symm) p =
@[simp]
theorem gen_loop.loop_homeo_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (p : (gen_loop N X x)) :
p =
theorem gen_loop.to_loop_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p : (gen_loop N X x)} {t : unit_interval} {tn : {j // j i} unit_interval} :
( p) t) tn = p ( (t, tn))
theorem gen_loop.from_loop_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p : loop_space (gen_loop {j // j i} X x) gen_loop.const} {t : N unit_interval} :
p) t = (p (t i)) ( t).snd
@[reducible]
def gen_loop.c_comp_insert {N : Type u_1} {X : Type u_2} [decidable_eq N] (i : N) :

Composition with cube.insert_at as a continuous map.

Equations
def gen_loop.homotopy_to {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : p.val.homotopy_rel q.val ) :

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
theorem gen_loop.homotopy_to_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : p.val.homotopy_rel q.val ) (tₙ : {j // j i} unit_interval) :
( H) t) tₙ = H (t.fst, (t.snd, tₙ))
theorem gen_loop.homotopic_to {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} :
q)
def gen_loop.homotopy_from {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : q)) :

The converse to gen_loop.homotopy_to: 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
theorem gen_loop.homotopy_from_apply {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : q)) (t : unit_interval × ) :
t = (H (t.fst, t.snd i)) (λ (j : {j // j i}), t.snd j)
theorem gen_loop.homotopic_from {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} :
q)
noncomputable def gen_loop.trans_at {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (f g : (gen_loop N X x)) :
(gen_loop N X x)

Concatenation of two gen_loops along the ith coordinate.

Equations
def gen_loop.symm_at {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) (f : (gen_loop N X x)) :
(gen_loop N X x)

Reversal of a gen_loop along the ith coordinate.

Equations
theorem gen_loop.trans_at_distrib {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] {i j : N} (h : i j) (a b c d : (gen_loop N X x)) :
b) d) = c) d)
theorem gen_loop.from_loop_trans_to_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] {i : N} {p q : (gen_loop N X x)} :
(path.trans p) q)) = q
theorem gen_loop.from_loop_symm_to_loop {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] {i : N} {p : (gen_loop N X x)} :
(path.symm p)) =
def homotopy_group (N : Type u_1) (X : Type u_2) (x : X) :
Type (max u_1 u_2)

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

Equations
• x =
Instances for homotopy_group
@[protected, instance]
def homotopy_group.inhabited (N : Type u_1) (X : Type u_2) (x : X) :
noncomputable def homotopy_group_equiv_fundamental_group {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :

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

Equations
@[reducible]
def homotopy_group.pi (n : ) (X : Type u_1) (x : X) :
Type u_1

Homotopy group of finite index.

Equations
• x = X x
def gen_loop_homeo_of_is_empty {X : Type u_2} (N : Type u_1) (x : X) [is_empty N] :

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

Equations
def homotopy_group_equiv_zeroth_homotopy_of_is_empty {X : Type u_2} (N : Type u_1) (x : X) [is_empty N] :
x

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

Equations

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

Equations
@[simp]
theorem gen_loop_equiv_of_unique_symm_apply_coe_apply {X : Type u_2} {x : X} (N : Type u_1) [unique N] (p : x) (c : N unit_interval) :
(.symm) p) c = p
@[simp]
theorem gen_loop_equiv_of_unique_apply_apply {X : Type u_2} {x : X} (N : Type u_1) [unique N] (p : (gen_loop N X x)) (t : unit_interval) :
p) t = p (λ (_x : N), t)
def gen_loop_equiv_of_unique {X : Type u_2} {x : X} (N : Type u_1) [unique N] :
(gen_loop N X x) x

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

Equations
noncomputable def homotopy_group_equiv_fundamental_group_of_unique {X : Type u_2} {x : X} (N : Type u_1) [unique N] :
x

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
noncomputable def homotopy_group.pi_1_equiv_fundamental_group {X : Type u_2} {x : X} :
x

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

Equations
@[protected, instance]
noncomputable def homotopy_group.group {X : Type u_2} {x : X} (N : Type u_1) [decidable_eq N] [nonempty N] :
group X x)

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

Equations
@[reducible]
noncomputable def homotopy_group.aux_group {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :
group X x)

Group structure on homotopy_group 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
theorem homotopy_group.is_unital_aux_group {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i : N) :
theorem homotopy_group.aux_group_indep {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] (i j : N) :
theorem homotopy_group.trans_at_indep {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] {i : N} (j : N) (f g : (gen_loop N X x)) :
theorem homotopy_group.symm_at_indep {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] {i : N} (j : N) (f : (gen_loop N X x)) :
theorem homotopy_group.one_def {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] [nonempty N] :

Characterization of multiplicative identity

theorem homotopy_group.mul_spec {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] [nonempty N] {i : N} {p q : (gen_loop N X x)} :

Characterization of multiplication

theorem homotopy_group.inv_spec {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] [nonempty N] {i : N} {p : (gen_loop N X x)} :

Characterization of multiplicative inverse

@[protected, instance]
noncomputable def homotopy_group.comm_group {N : Type u_1} {X : Type u_2} {x : X} [decidable_eq N] [nontrivial N] :

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

Equations