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.

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

The n-dimensional cube.

Equations
Instances for cube
@[protected, instance]
def cube.has_zero (n : ) :
@[protected, instance]
@[continuity]
theorem cube.proj_continuous {n : } (i : fin n) :
continuous (λ (f : cube n), f i)
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
@[simp]
def cube.head {n : } :

The first projection of a positive-dimensional cube.

Equations
@[continuity]
@[simp]
def cube.tail {n : } :
cube (n + 1)cube n

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

Equations
@[protected, instance]
Equations
theorem cube.one_char (f : cube 1) :
f = λ (_x : fin 1), f 0
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
@[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
@[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
@[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 nf.to_fun y = x) (y : cube n) :
def gen_loop.const {X : Type u} [topological_space X] {n : } {x : X} :

The constant gen_loop at x.

Equations
@[protected, instance]
def gen_loop.inhabited {X : Type u} [topological_space X] {n : } {x : X} :
Equations
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
@[refl]
theorem gen_loop.homotopic.refl {X : Type u} [topological_space X] {n : } {x : X} (f : gen_loop n x) :
@[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) :
@[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) :
@[protected, instance]
def gen_loop.homotopic.setoid {X : Type u} [topological_space X] (n : ) (x : X) :
Equations
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
@[protected, instance]
def homotopy_group.inhabited {X : Type u} [topological_space X] (n : ) (x : X) :
def gen_loop_zero_equiv {X : Type u} [topological_space X] {x : X} :

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

Equations

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

Equations
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
@[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) :
noncomputable def pi1_equiv_fundamental_group {X : Type u} [topological_space X] {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