mathlib3 documentation

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 #

TODO:

def cube.boundary (N : Type u_1) :

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

Equations
@[reducible]

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

Equations
@[reducible]

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}) :
@[reducible]
def loop_space (X : Type u_2) [topological_space X] (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) [topological_space X] (x : X) :
Equations
def gen_loop (N : Type u_1) (X : Type u_2) [topological_space X] (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} [topological_space X] {x : X} (f : (gen_loop N X x)) (g : (N unit_interval) 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} [topological_space X] {x : X} (f : (gen_loop N X x)) {g : (N unit_interval) X} (h : g = f) :
theorem gen_loop.copy_eq {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} (f : (gen_loop N X x)) {g : (N unit_interval) X} (h : g = f) :
theorem gen_loop.boundary {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} (f : (gen_loop N X x)) (y : N unit_interval) (H : y cube.boundary N) :
f y = x
@[protected, instance]
def gen_loop.fun_like {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} :
Equations
@[ext]
theorem gen_loop.ext {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} (f g : (gen_loop N X x)) (H : (y : N unit_interval), f y = g y) :
f = g
@[simp]
theorem gen_loop.mk_apply {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} (f : C(N unit_interval, X)) (H : f gen_loop N X x) (y : N unit_interval) :
f, H⟩ y = f y
def gen_loop.const {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {x : X} {t : N unit_interval} :
@[protected, instance]
def gen_loop.inhabited {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} :
Equations
def gen_loop.homotopic {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {x : X} (f : (gen_loop N X x)) :
@[symm]
theorem gen_loop.homotopic.symm {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} {f g : (gen_loop N X x)} (H : gen_loop.homotopic f g) :
@[trans]
theorem gen_loop.homotopic.trans {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} {f g h : (gen_loop N X x)} (H0 : gen_loop.homotopic f g) (H1 : gen_loop.homotopic g h) :
@[protected, instance]
def gen_loop.homotopic.setoid {X : Type u_2} [topological_space X] (N : Type u_1) (x : X) :
Equations
def gen_loop.to_loop {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {x : X} [decidable_eq N] (i : N) (p : (gen_loop N X x)) (t : unit_interval) :
theorem gen_loop.continuous_to_loop {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) :
def gen_loop.from_loop {N : Type u_1} {X : Type u_2} [topological_space X] {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
theorem gen_loop.continuous_from_loop {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) :
theorem gen_loop.to_from {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
def gen_loop.loop_homeo {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {x : X} [decidable_eq N] (i : N) (p : loop_space (gen_loop {j // j i} X x) gen_loop.const) :
@[simp]
theorem gen_loop.loop_homeo_apply {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) (p : (gen_loop N X x)) :
theorem gen_loop.to_loop_apply {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) {p : (gen_loop N X x)} {t : unit_interval} {tn : {j // j i} unit_interval} :
((gen_loop.to_loop i p) t) tn = p ((cube.insert_at i) (t, tn))
theorem gen_loop.from_loop_apply {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) {p : loop_space (gen_loop {j // j i} X x) gen_loop.const} {t : N unit_interval} :
@[reducible]

Composition with cube.insert_at as a continuous map.

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

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} [topological_space X] {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : p.val.homotopy_rel q.val (cube.boundary N)) (t : unit_interval × unit_interval) (tₙ : {j // j i} unit_interval) :
((gen_loop.homotopy_to i H) t) tₙ = H (t.fst, (cube.insert_at i) (t.snd, tₙ))
theorem gen_loop.homotopic_to {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} :
def gen_loop.homotopy_from {N : Type u_1} {X : Type u_2} [topological_space X] {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : path.homotopy (gen_loop.to_loop i p) (gen_loop.to_loop i 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} [topological_space X] {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} (H : path.homotopy (gen_loop.to_loop i p) (gen_loop.to_loop i q)) (t : unit_interval × (N unit_interval)) :
(gen_loop.homotopy_from i H) 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} [topological_space X] {x : X} [decidable_eq N] (i : N) {p q : (gen_loop N X x)} :
noncomputable def gen_loop.trans_at {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {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} [topological_space X] {x : X} [decidable_eq N] {i j : N} (h : i j) (a b c d : (gen_loop N X x)) :
def homotopy_group (N : Type u_1) (X : Type u_2) [topological_space X] (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
Instances for homotopy_group
@[protected, instance]
def homotopy_group.inhabited (N : Type u_1) (X : Type u_2) [topological_space X] (x : X) :
noncomputable def homotopy_group_equiv_fundamental_group {N : Type u_1} {X : Type u_2} [topological_space X] {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) [topological_space X] (x : X) :
Type u_1

Homotopy group of finite index.

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

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

Equations

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

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

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} [topological_space X] {x : X} (N : Type u_1) [unique N] :

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

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} [topological_space X] {x : X} (N : Type u_1) [decidable_eq N] [nonempty N] :

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} [topological_space X] {x : X} [decidable_eq N] (i : N) :

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.trans_at_indep {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {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} [topological_space X] {x : X} [decidable_eq N] [nonempty N] :

Characterization of multiplicative identity

theorem homotopy_group.mul_spec {N : Type u_1} {X : Type u_2} [topological_space X] {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} [topological_space X] {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} [topological_space X] {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