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 xis the type of continuous fuctionsI^N → Xthat send the boundary tox,homotopy_group.pi n X xdenotedπ_ n X xis the quotient ofgen_loop (fin n) xby 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 XwhenM ≃ N. Similarly forπ_.- Path-induced homomorphisms. Show that
homotopy_group.pi_1_equiv_fundamental_groupis a group isomorphism. - Examples with
𝕊^n:π_n (𝕊^n) = ℤ,π_m (𝕊^n)trivial form < n. - Actions of π_1 on π_n.
- Lie algebra:
⁅π_(n+1), π_(m+1)⁆contained inπ_(n+m+1).
The points in a cube with at least one projection equal to 0 or 1.
Equations
- cube.boundary N = {y : N → ↥unit_interval | ∃ (i : N), y i = 0 ∨ y i = 1}
@[reducible]
def
cube.split_at
{N : Type u_1}
[decidable_eq N]
(i : N) :
(N → ↥unit_interval) ≃ₜ ↥unit_interval × ({j // j ≠ i} → ↥unit_interval)
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) :
↥unit_interval × ({j // j ≠ i} → ↥unit_interval) ≃ₜ (N → ↥unit_interval)
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}) :
⇑(cube.insert_at i) (t₀, t) ∈ cube.boundary N
@[reducible]
The space of paths with both endpoints equal to a specified point x : X.
Equations
- loop_space X x = path x x
@[protected, instance]
Equations
- loop_space.inhabited X x = {default := path.refl 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) :
Copy of a gen_loop with a new map from the unit cube equal to the old one.
Useful to fix definitional equalities.
Equations
- gen_loop.copy f g h = ⟨{to_fun := g, continuous_to_fun := _}, _⟩
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) :
⇑(gen_loop.copy f g h) = g
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) :
gen_loop.copy f g h = 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) :
@[protected, instance]
def
gen_loop.fun_like
{N : Type u_1}
{X : Type u_2}
[topological_space X]
{x : X} :
fun_like ↥(gen_loop N X x) (N → ↥unit_interval) (λ (_x : N → ↥unit_interval), X)
Equations
- gen_loop.fun_like = {coe := λ (f : ↥(gen_loop N X x)), ⇑(f.val), coe_injective' := _}
@[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) :
The constant gen_loop at x.
Equations
- gen_loop.const = ⟨continuous_map.const (N → ↥unit_interval) x, _⟩
@[simp]
theorem
gen_loop.const_apply
{N : Type u_1}
{X : Type u_2}
[topological_space X]
{x : X}
{t : N → ↥unit_interval} :
⇑gen_loop.const t = x
@[protected, instance]
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
- gen_loop.homotopic f g = f.val.homotopic_rel g.val (cube.boundary N)
@[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]
Equations
- gen_loop.homotopic.setoid N x = {r := gen_loop.homotopic x, iseqv := _}
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_space ↥(gen_loop {j // j ≠ i} X x) gen_loop.const
Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus\{j\}} → X)$.
Equations
- gen_loop.to_loop i p = {to_continuous_map := {to_fun := λ (t : ↥unit_interval), ⟨⇑((p.val.comp (cube.insert_at i).to_continuous_map).curry) t, _⟩, continuous_to_fun := _}, source' := _, target' := _}
@[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) :
↑(⇑(gen_loop.to_loop i p) t) = ⇑((p.val.comp (cube.insert_at i).to_continuous_map).curry) t
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) :
Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$.
Equations
- gen_loop.from_loop i p = ⟨({to_fun := coe coe_to_lift, continuous_to_fun := _}.comp p.to_continuous_map).uncurry.comp (cube.split_at i).to_continuous_map, _⟩
@[simp]
theorem
gen_loop.from_loop_coe
{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.from_loop i p) = ({to_fun := coe coe_to_lift, continuous_to_fun := _}.comp p.to_continuous_map).uncurry.comp (cube.split_at i).to_continuous_map
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) :
gen_loop.to_loop i (gen_loop.from_loop i p) = p
def
gen_loop.loop_homeo
{N : Type u_1}
{X : Type u_2}
[topological_space X]
{x : X}
[decidable_eq N]
(i : N) :
↥(gen_loop N X x) ≃ₜ loop_space ↥(gen_loop {j // j ≠ i} X x) gen_loop.const
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
- gen_loop.loop_homeo i = {to_equiv := {to_fun := gen_loop.to_loop i, inv_fun := gen_loop.from_loop i, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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) :
⇑((gen_loop.loop_homeo i).symm) p = gen_loop.from_loop i p
@[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)) :
⇑(gen_loop.loop_homeo i) p = gen_loop.to_loop i p
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} :
⇑(gen_loop.from_loop i p) t = ⇑(⇑p (t i)) (⇑(cube.split_at i) t).snd
@[reducible]
def
gen_loop.c_comp_insert
{N : Type u_1}
{X : Type u_2}
[topological_space X]
[decidable_eq N]
(i : N) :
Composition with cube.insert_at as a continuous map.
Equations
- gen_loop.c_comp_insert i = {to_fun := λ (f : C(N → ↥unit_interval, X)), f.comp (cube.insert_at i).to_continuous_map, continuous_to_fun := _}
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)) :
C(↥unit_interval × ↥unit_interval, C({j // j ≠ i} → ↥unit_interval, X))
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
- gen_loop.homotopy_to i H = ({to_fun := continuous_map.curry _inst_1, continuous_to_fun := _}.comp ((gen_loop.c_comp_insert i).comp H.to_homotopy.to_continuous_map.curry)).uncurry
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)} :
gen_loop.homotopic p q → path.homotopic (gen_loop.to_loop i p) (gen_loop.to_loop i q)
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)) :
C(↥unit_interval × (N → ↥unit_interval), X)
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
- gen_loop.homotopy_from i H = ({to_fun := continuous_map.uncurry _, continuous_to_fun := _}.comp ({to_fun := coe coe_to_lift, continuous_to_fun := _}.comp H.to_homotopy.to_continuous_map).curry).uncurry.comp ((continuous_map.id ↥unit_interval).prod_map (cube.split_at i).to_continuous_map)
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)) :
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)} :
path.homotopic (gen_loop.to_loop i p) (gen_loop.to_loop i q) → gen_loop.homotopic p q
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)) :
Concatenation of two gen_loops along the ith coordinate.
Equations
- gen_loop.trans_at i f g = gen_loop.copy (gen_loop.from_loop i (path.trans (gen_loop.to_loop i f) (gen_loop.to_loop i g))) (λ (t : N → ↥unit_interval), ite (↑(t i) ≤ 1 / 2) (⇑f (function.update t i (set.proj_Icc 0 1 gen_loop.trans_at._proof_1 (2 * ↑(t i))))) (⇑g (function.update t i (set.proj_Icc 0 1 gen_loop.trans_at._proof_2 (2 * ↑(t i) - 1))))) _
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)) :
Reversal of a gen_loop along the ith coordinate.
Equations
- gen_loop.symm_at i f = gen_loop.copy (gen_loop.from_loop i (path.symm (gen_loop.to_loop i f))) (λ (t : N → ↥unit_interval), ⇑f (λ (j : N), ite (j = i) (unit_interval.symm (t i)) (t j))) _
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)) :
gen_loop.trans_at i (gen_loop.trans_at j a b) (gen_loop.trans_at j c d) = gen_loop.trans_at j (gen_loop.trans_at i a c) (gen_loop.trans_at i b d)
theorem
gen_loop.from_loop_trans_to_loop
{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)} :
gen_loop.from_loop i (path.trans (gen_loop.to_loop i p) (gen_loop.to_loop i q)) = gen_loop.trans_at i p q
theorem
gen_loop.from_loop_symm_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)} :
gen_loop.from_loop i (path.symm (gen_loop.to_loop i p)) = gen_loop.symm_at i p
The nth homotopy group at x defined as the quotient of Ω^n x by the
gen_loop.homotopic relation.
Equations
- homotopy_group N X x = quotient (gen_loop.homotopic.setoid N x)
Instances for homotopy_group
@[protected, instance]
def
homotopy_group.inhabited
(N : Type u_1)
(X : Type u_2)
[topological_space X]
(x : X) :
inhabited (homotopy_group N 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) :
homotopy_group N X x ≃ fundamental_group ↥(gen_loop {j // j ≠ i} X x) gen_loop.const
Equivalence between the homotopy group of X and the fundamental group of
Ω^{j // j ≠ i} x.
@[reducible]
Homotopy group of finite index.
Equations
- homotopy_group.pi n X x = homotopy_group (fin n) X x
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
- gen_loop_homeo_of_is_empty N x = {to_equiv := {to_fun := λ (f : ↥(gen_loop N X x)), ⇑f 0, inv_fun := λ (y : X), ⟨continuous_map.const (N → ↥unit_interval) y, _⟩, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homotopy_group_equiv_zeroth_homotopy_of_is_empty
{X : Type u_2}
[topological_space X]
(N : Type u_1)
(x : X)
[is_empty N] :
homotopy_group N X x ≃ zeroth_homotopy X
The homotopy "group" indexed by an empty type is in bijection with
the path components of X, aka the zeroth_homotopy.
Equations
def
homotopy_group.pi_0_equiv_zeroth_homotopy
{X : Type u_2}
[topological_space X]
{x : X} :
homotopy_group.pi 0 X x ≃ zeroth_homotopy X
The 0th homotopy "group" is in bijection with zeroth_homotopy.
@[simp]
theorem
gen_loop_equiv_of_unique_symm_apply_coe_apply
{X : Type u_2}
[topological_space X]
{x : X}
(N : Type u_1)
[unique N]
(p : loop_space X x)
(c : N → ↥unit_interval) :
⇑↑(⇑((gen_loop_equiv_of_unique N).symm) p) c = ⇑p (c inhabited.default)
@[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] :
↥(gen_loop N X x) ≃ loop_space X x
The 1-dimensional generalized loops based at x are in bijection with loops at x.
Equations
- gen_loop_equiv_of_unique N = {to_fun := λ (p : ↥(gen_loop N X x)), {to_continuous_map := {to_fun := λ (t : ↥unit_interval), ⇑p (λ (_x : N), t), continuous_to_fun := _}, source' := _, target' := _}, inv_fun := λ (p : loop_space X x), ⟨{to_fun := λ (c : N → ↥unit_interval), ⇑p (c inhabited.default), continuous_to_fun := _}, _⟩, left_inv := _, right_inv := _}
noncomputable
def
homotopy_group_equiv_fundamental_group_of_unique
{X : Type u_2}
[topological_space X]
{x : X}
(N : Type u_1)
[unique N] :
homotopy_group N X x ≃ fundamental_group X 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.
noncomputable
def
homotopy_group.pi_1_equiv_fundamental_group
{X : Type u_2}
[topological_space X]
{x : X} :
homotopy_group.pi 1 X x ≃ fundamental_group X x
The first homotopy group at x is in bijection with the fundamental group.
@[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 (homotopy_group N 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}
[topological_space X]
{x : X}
[decidable_eq N]
(i : N) :
group (homotopy_group N 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}
[topological_space X]
{x : X}
[decidable_eq N]
(i : N) :
theorem
homotopy_group.aux_group_indep
{N : Type u_1}
{X : Type u_2}
[topological_space X]
{x : X}
[decidable_eq N]
(i j : N) :
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)) :
⟦gen_loop.trans_at i f g⟧ = ⟦gen_loop.trans_at j f g⟧
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)) :
⟦gen_loop.symm_at i f⟧ = ⟦gen_loop.symm_at j f⟧
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] :
comm_group (homotopy_group N X x)
Multiplication on homotopy_group N X x is commutative for nontrivial N.
In particular, multiplication on π_(n+2) is commutative.
Equations
- homotopy_group.comm_group = let h : ∃ (y : N), y ≠ classical.arbitrary N := homotopy_group.comm_group._proof_1 in eckmann_hilton.comm_group homotopy_group.comm_group._proof_2 homotopy_group.comm_group._proof_3