mathlib documentation

topology.homotopy.homotopy_group

nth homotopy group #

We define the nth homotopy group at x, π n x, as the equivalence classes of functions from the nth 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 n x, in particular gen_loop 1 x ≃ path x x

We show that π 0 x is equivalent to the path-conected components, and that π 1 x is equivalent to the fundamental group at x.

definitions #

TODO: show that π n x is a group when n > 0 and abelian when n > 1. Show that pi1_equiv_fundamental_group is an isomorphism of groups.

source
@[protected, instance]
def cube.has_one (n : ℕ) :
has_one (cube n)
source
def cube (n : ℕ) :
Type

The n-dimensional cube.

Equations
Instances for cube
source
@[protected, instance]
def cube.has_zero (n : ℕ) :
has_zero (cube n)
source
@[protected, instance]
def cube.topological_space (n : ℕ) :
topological_space (cube n)
source
@[continuity]
theorem cube.proj_continuous {n : ℕ} (i : fin n) :
continuous (λ (f : cube n), f i)
source
def cube.boundary (n : ℕ) :
set (cube n)

The points of the n-dimensional cube with at least one projection equal to 0 or 1.

Equations
source
@[simp]
def cube.head {n : ℕ} :
cube (n + 1) → ↥unit_interval

The first projection of a positive-dimensional cube.

Equations
source
@[continuity]
theorem cube.head.continuous {n : ℕ} :
continuous cube.head
source
@[simp]
def cube.tail {n : ℕ} :
cube (n + 1) → cube n

The projection to the last n coordinates from an n+1 dimensional cube.

Equations
source
@[protected, instance]
def cube.unique_cube0  :
unique (cube 0)
Equations
source
theorem cube.one_char (f : cube 1) :
f = λ (_x : fin 1), f 0
source
structure gen_loop {X : Type u} [topological_space X] (n : ℕ) (x : X) :
Type u

The n-dimensional generalized loops; functions I^n → X that send the boundary to the base point.

Instances for gen_loop
source
@[protected, instance]
def gen_loop.fun_like {X : Type u} [topological_space X] {n : ℕ} {x : X} :
fun_like (gen_loop n x) (cube n) (λ (_x : cube n), X)
Equations
source
@[ext]
theorem gen_loop.ext {X : Type u} [topological_space X] {n : ℕ} {x : X} (f g : gen_loop n x) (H : ∀ (y : cube n), ⇑f y = ⇑g y) :
f = g
source
@[simp]
theorem gen_loop.mk_apply {X : Type u} [topological_space X] {n : ℕ} {x : X} (f : C(cube n, X)) (H : ∀ (y : cube n), y ∈ cube.boundary n → f.to_fun y = x) (y : cube n) :
⇑{to_continuous_map := f, boundary := H} y = ⇑f y
source
def gen_loop.const {X : Type u} [topological_space X] {n : ℕ} {x : X} :
gen_loop n x

The constant gen_loop at x.

Equations
source
@[protected, instance]
def gen_loop.inhabited {X : Type u} [topological_space X] {n : ℕ} {x : X} :
inhabited (gen_loop n x)
Equations
source
def gen_loop.homotopic {X : Type u} [topological_space X] {n : ℕ} {x : X} (f g : gen_loop n x) :
Prop

The "homotopy relative to boundary" relation between gen_loops.

Equations
source
@[refl]
theorem gen_loop.homotopic.refl {X : Type u} [topological_space X] {n : ℕ} {x : X} (f : gen_loop n x) :
f.homotopic f
source
@[symm]
theorem gen_loop.homotopic.symm {X : Type u} [topological_space X] {n : ℕ} {x : X} {f g : gen_loop n x} (H : f.homotopic g) :
g.homotopic f
source
@[trans]
theorem gen_loop.homotopic.trans {X : Type u} [topological_space X] {n : ℕ} {x : X} {f g h : gen_loop n x} (H0 : f.homotopic g) (H1 : g.homotopic h) :
f.homotopic h
source
theorem gen_loop.homotopic.equiv {X : Type u} [topological_space X] {n : ℕ} {x : X} :
equivalence gen_loop.homotopic
source
@[protected, instance]
def gen_loop.homotopic.setoid {X : Type u} [topological_space X] (n : ℕ) (x : X) :
setoid (gen_loop n x)
Equations
source
def homotopy_group {X : Type u} [topological_space X] (n : ℕ) (x : X) :
Type u

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

Equations
Instances for homotopy_group
source
@[protected, instance]
def homotopy_group.inhabited {X : Type u} [topological_space X] (n : ℕ) (x : X) :
inhabited (homotopy_group n x)
source
def gen_loop_zero_equiv {X : Type u} [topological_space X] {x : X} :
gen_loop 0 x ≃ X

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

Equations
source
def pi0_equiv_path_components {X : Type u} [topological_space X] {x : X} :
homotopy_group 0 x ≃ zeroth_homotopy X

The 0th homotopy "group" is equivalent to the path components of X, aka the zeroth_homotopy.

Equations
source
def gen_loop_one_equiv_path_self {X : Type u} [topological_space X] {x : X} :
gen_loop 1 x ≃ path x x

The 1-dimensional generalized loops based at x are in 1-1 correspondence with paths from x to itself.

Equations
source
@[simp]
theorem gen_loop_one_equiv_path_self_apply_apply {X : Type u} [topological_space X] {x : X} (p : gen_loop 1 x) (t : ↥unit_interval) :
⇑(⇑gen_loop_one_equiv_path_self p) t = ⇑p (λ (_x : fin 1), t)
source
@[simp]
theorem gen_loop_one_equiv_path_self_symm_apply_to_continuous_map_apply {X : Type u} [topological_space X] {x : X} (p : path x x) (c : cube 1) :
⇑((⇑(gen_loop_one_equiv_path_self.symm) p).to_continuous_map) c = ⇑p c.head
source
noncomputable def pi1_equiv_fundamental_group {X : Type u} [topological_space X] {x : X} :
homotopy_group 1 x ≃ fundamental_group X x

The first homotopy group at x is equivalent to the fundamental group, i.e. the loops based at x up to homotopy.

Equations