n
th homotopy group #
We define the n
th 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 #
gen_loop n x
is the type of continous fuctionsI^n → X
that send the boundary tox
homotopy_group n x
denotedπ n x
is the quotient ofgen_loop n x
by homotopy relative to the boundary
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.
The n
-dimensional cube.
Instances for cube
Equations
- cube.unique_cube0 = pi.unique_of_is_empty (λ (ᾰ : fin 0), ↥unit_interval)
- to_continuous_map : C(cube n, X)
- boundary : ∀ (y : cube n), y ∈ cube.boundary n → self.to_continuous_map.to_fun y = x
The n
-dimensional generalized loops; functions I^n → X
that send the boundary to the base point.
Instances for gen_loop
- gen_loop.has_sizeof_inst
- gen_loop.fun_like
- gen_loop.inhabited
- gen_loop.homotopic.setoid
Equations
- gen_loop.fun_like = {coe := λ (f : gen_loop n x), ⇑(f.to_continuous_map), coe_injective' := _}
The constant gen_loop
at x
.
Equations
- gen_loop.const = {to_continuous_map := continuous_map.const (cube n) x, boundary := _}
Equations
The "homotopy relative to boundary" relation between gen_loop
s.
Equations
Equations
- gen_loop.homotopic.setoid n x = {r := gen_loop.homotopic x, iseqv := _}
The n
th homotopy group at x
defined as the quotient of gen_loop n x
by the
homotopic
relation.
Equations
- homotopy_group n x = quotient (gen_loop.homotopic.setoid n x)
Instances for homotopy_group
The 0-dimensional generalized loops based at x
are in 1-1 correspondence with X
.
Equations
- gen_loop_zero_equiv = {to_fun := λ (f : gen_loop 0 x), ⇑f 0, inv_fun := λ (x_1 : X), {to_continuous_map := continuous_map.const (cube 0) x_1, boundary := _}, left_inv := _, right_inv := _}
The 0th homotopy "group" is equivalent to the path components of X
, aka the zeroth_homotopy
.
Equations
- pi0_equiv_path_components = quotient.congr gen_loop_zero_equiv pi0_equiv_path_components._proof_1
The 1-dimensional generalized loops based at x
are in 1-1 correspondence with
paths from x
to itself.
Equations
- gen_loop_one_equiv_path_self = {to_fun := λ (p : gen_loop 1 x), {to_continuous_map := {to_fun := λ (t : ↥unit_interval), ⇑p (λ (_x : fin 1), t), continuous_to_fun := _}, source' := _, target' := _}, inv_fun := λ (p : path x x), {to_continuous_map := {to_fun := λ (c : cube 1), ⇑p c.head, continuous_to_fun := _}, boundary := _}, left_inv := _, right_inv := _}
The first homotopy group at x
is equivalent to the fundamental group,
i.e. the loops based at x
up to homotopy.
Equations
- pi1_equiv_fundamental_group = (quotient.congr gen_loop_one_equiv_path_self pi1_equiv_fundamental_group._proof_1).trans (category_theory.groupoid.iso_equiv_hom x x).symm