Documentation

Mathlib.Topology.Homotopy.HomotopyGroup

nth homotopy group #

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 GenLoop (Fin n) x; in particular GenLoop (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) :
Set (NunitInterval)

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

Equations
@[reducible, inline]
abbrev Cube.splitAt {N : Type u_1} [DecidableEq N] (i : N) :
(NunitInterval) ≃ₜ unitInterval × ({ j : N // j i }unitInterval)

The forward direction of the homeomorphism between the cube IN and I×IN{j}.

Equations
@[reducible, inline]
abbrev Cube.insertAt {N : Type u_1} [DecidableEq N] (i : N) :
unitInterval × ({ j : N // j i }unitInterval) ≃ₜ (NunitInterval)

The backward direction of the homeomorphism between the cube IN and I×IN{j}.

Equations
theorem Cube.insertAt_boundary {N : Type u_1} [DecidableEq N] (i : N) {t₀ : unitInterval} {t : { j : N // j i }unitInterval} (H : (t₀ = 0 t₀ = 1) t Cube.boundary { j : N // j i }) :
@[reducible, inline]
abbrev LoopSpace (X : Type u_2) [TopologicalSpace X] (x : X) :
Type u_2

The space of paths with both endpoints equal to a specified point x : X.

Equations
instance LoopSpace.inhabited (X : Type u_2) [TopologicalSpace X] (x : X) :
Equations
def GenLoop (N : Type u_1) (X : Type u_2) [TopologicalSpace 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

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
instance GenLoop.instFunLike {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
FunLike (↑(GenLoop N X x)) (NunitInterval) X
Equations
  • GenLoop.instFunLike = { coe := fun (f : (GenLoop N X x)) => f, coe_injective' := }
theorem GenLoop.ext {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) (g : (GenLoop N X x)) (H : ∀ (y : NunitInterval), f y = g y) :
f = g
@[simp]
theorem GenLoop.mk_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : C(NunitInterval, X)) (H : f GenLoop N X x) (y : NunitInterval) :
f, H y = f y
instance GenLoop.instContinuousEval {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
ContinuousEval (↑(GenLoop N X x)) (NunitInterval) X
Equations
  • =
instance GenLoop.instContinuousEvalConst {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
ContinuousEvalConst (↑(GenLoop N X x)) (NunitInterval) X
Equations
  • =
def GenLoop.copy {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) (g : (NunitInterval)X) (h : g = f) :
(GenLoop N X x)

Copy of a GenLoop with a new map from the unit cube equal to the old one. Useful to fix definitional equalities.

Equations
  • GenLoop.copy f g h = { toFun := g, continuous_toFun := },
theorem GenLoop.coe_copy {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) {g : (NunitInterval)X} (h : g = f) :
(GenLoop.copy f g h) = g
theorem GenLoop.copy_eq {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) {g : (NunitInterval)X} (h : g = f) :
GenLoop.copy f g h = f
theorem GenLoop.boundary {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) (y : NunitInterval) :
y Cube.boundary Nf y = x
def GenLoop.const {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
(GenLoop N X x)

The constant GenLoop at x.

Equations
@[simp]
theorem GenLoop.const_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {t : NunitInterval} :
GenLoop.const t = x
instance GenLoop.inhabited {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
Inhabited (GenLoop N X x)
Equations
  • GenLoop.inhabited = { default := GenLoop.const }
def GenLoop.Homotopic {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) (g : (GenLoop N X x)) :

The "homotopic relative to boundary" relation between GenLoops.

Equations
theorem GenLoop.Homotopic.refl {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : (GenLoop N X x)) :
theorem GenLoop.Homotopic.symm {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f : (GenLoop N X x)} {g : (GenLoop N X x)} (H : GenLoop.Homotopic f g) :
theorem GenLoop.Homotopic.trans {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f : (GenLoop N X x)} {g : (GenLoop N X x)} {h : (GenLoop N X x)} (H0 : GenLoop.Homotopic f g) (H1 : GenLoop.Homotopic g h) :
theorem GenLoop.Homotopic.equiv {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
Equivalence GenLoop.Homotopic
instance GenLoop.Homotopic.setoid {X : Type u_2} [TopologicalSpace X] (N : Type u_3) (x : X) :
Setoid (GenLoop N X x)
Equations
def GenLoop.toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : (GenLoop N X x)) :
LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const

Loop from a generalized loop by currying INX into I(IN{j}X).

Equations
@[simp]
theorem GenLoop.toLoop_apply_coe {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : (GenLoop N X x)) (t : unitInterval) :
((GenLoop.toLoop i p) t) = ((↑p).comp (Cube.insertAt i)).curry t
theorem GenLoop.continuous_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
def GenLoop.fromLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const) :
(GenLoop N X x)

Generalized loop from a loop by uncurrying I(IN{j}X) into INX.

Equations
@[simp]
theorem GenLoop.fromLoop_coe {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const) :
(GenLoop.fromLoop i p) = ({ toFun := Subtype.val, continuous_toFun := }.comp p.toContinuousMap).uncurry.comp (Cube.splitAt i)
theorem GenLoop.continuous_fromLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
theorem GenLoop.to_from {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const) :
def GenLoop.loopHomeo {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
(GenLoop N X x) ≃ₜ LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.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
@[simp]
theorem GenLoop.loopHomeo_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : (GenLoop N X x)) :
@[simp]
theorem GenLoop.loopHomeo_symm_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const) :
theorem GenLoop.toLoop_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {t : unitInterval} {tn : { j : N // j i }unitInterval} :
((GenLoop.toLoop i p) t) tn = p ((Cube.insertAt i) (t, tn))
theorem GenLoop.fromLoop_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : LoopSpace (↑(GenLoop { j : N // j i } X x)) GenLoop.const} {t : NunitInterval} :
(GenLoop.fromLoop i p) t = (p (t i)) ((Cube.splitAt i) t).2
@[reducible, inline]
abbrev GenLoop.cCompInsert {N : Type u_1} {X : Type u_2} [TopologicalSpace X] [DecidableEq N] (i : N) :
C(C(NunitInterval, X), C(unitInterval × ({ j : N // j i }unitInterval), X))

Composition with Cube.insertAt as a continuous map.

Equations
def GenLoop.homotopyTo {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) :
C(unitInterval × unitInterval, C({ j : N // j i }unitInterval, 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
theorem GenLoop.homotopyTo_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) (t : unitInterval × unitInterval) (tₙ : { j : N // j i }unitInterval) :
((GenLoop.homotopyTo i H) t) tₙ = H (t.1, (Cube.insertAt i) (t.2, tₙ))
theorem GenLoop.homotopicTo {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
def GenLoop.homotopyFrom {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q)) :

The converse to GenLoop.homotopyTo: 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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem GenLoop.homotopyFrom_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} (H : Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q)) :
∀ (a : unitInterval × (NunitInterval)), (GenLoop.homotopyFrom i H) a = Function.uncurry (fun (x_1 : unitInterval) (y : unitInterval × ({ j : N // ¬j = i }unitInterval)) => Function.uncurry (fun (x_2 : unitInterval) (y : { j : N // ¬j = i }unitInterval) => (H (x_1, x_2)) y) y) (Prod.map id (⇑(Cube.splitAt i)) a)
theorem GenLoop.homotopicFrom {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
def GenLoop.transAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f : (GenLoop N X x)) (g : (GenLoop N X x)) :
(GenLoop N X x)

Concatenation of two GenLoops along the ith coordinate.

Equations
  • One or more equations did not get rendered due to their size.
def GenLoop.symmAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f : (GenLoop N X x)) :
(GenLoop N X x)

Reversal of a GenLoop along the ith coordinate.

Equations
theorem GenLoop.transAt_distrib {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} {j : N} (h : i j) (a : (GenLoop N X x)) (b : (GenLoop N X x)) (c : (GenLoop N X x)) (d : (GenLoop N X x)) :
theorem GenLoop.fromLoop_trans_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
theorem GenLoop.fromLoop_symm_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} {p : (GenLoop N X x)} :
def HomotopyGroup (N : Type u_3) (X : Type u_4) [TopologicalSpace X] (x : X) :
Type (max u_3 u_4)

The nth homotopy group at x defined as the quotient of Ω^n x by the GenLoop.Homotopic relation.

Equations
instance instInhabitedHomotopyGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
Equations
def homotopyGroupEquivFundamentalGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
HomotopyGroup N X x FundamentalGroup (↑(GenLoop { j : N // j i } X x)) GenLoop.const

Equivalence between the homotopy group of X and the fundamental group of Ω^{j // j ≠ i} x.

Equations
@[reducible, inline]
abbrev HomotopyGroup.Pi (n : ) (X : Type u_3) [TopologicalSpace X] (x : X) :
Type u_3

Homotopy group of finite index.

Equations
def genLoopHomeoOfIsEmpty {X : Type u_2} [TopologicalSpace X] (N : Type u_3) (x : X) [IsEmpty N] :
(GenLoop N X x) ≃ₜ X

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations

The 0th homotopy "group" is in bijection with ZerothHomotopy.

Equations
def genLoopEquivOfUnique {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] :
(GenLoop N X x) LoopSpace X x

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

Equations
  • One or more equations did not get rendered due to their size.

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
instance HomotopyGroup.group {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [DecidableEq N] [Nonempty N] :

Group structure on HomotopyGroup N X x for nonempty N (in particular π_(n+1) X x).

Equations
@[reducible, inline]
abbrev HomotopyGroup.auxGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :

Group structure on HomotopyGroup 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 HomotopyGroup.isUnital_auxGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
EckmannHilton.IsUnital Mul.mul GenLoop.const
theorem HomotopyGroup.transAt_indep {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} (j : N) (f : (GenLoop N X x)) (g : (GenLoop N X x)) :
GenLoop.transAt i f g = GenLoop.transAt j f g
theorem HomotopyGroup.symmAt_indep {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} (j : N) (f : (GenLoop N X x)) :
GenLoop.symmAt i f = GenLoop.symmAt j f
theorem HomotopyGroup.one_def {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] :
1 = GenLoop.const

Characterization of multiplicative identity

theorem HomotopyGroup.mul_spec {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] {i : N} {p : (GenLoop N X x)} {q : (GenLoop N X x)} :
(fun (x1 x2 : HomotopyGroup N X x) => x1 * x2) p q = GenLoop.transAt i q p

Characterization of multiplication

theorem HomotopyGroup.inv_spec {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] {i : N} {p : (GenLoop N X x)} :
(⟦p⟧)⁻¹ = GenLoop.symmAt i p

Characterization of multiplicative inverse

instance HomotopyGroup.commGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nontrivial N] :

Multiplication on HomotopyGroup N X x is commutative for nontrivial N. In particular, multiplication on π_(n+2) is commutative.

Equations