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

• GenLoop N x is the type of continuous functions I^N → X that send the boundary to x,
• HomotopyGroup.Pi n X x denoted π_ n X x is the quotient of GenLoop (Fin n) x by homotopy relative to the boundary,
• group instance Group (π_(n+1) X x),
• commutative group instance CommGroup (π_(n+2) X x).

TODO:

• Ω^M (Ω^N X) ≃ₜ Ω^(M⊕N) X, and Ω^M X ≃ₜ Ω^N X when M ≃ N. Similarly for π_.
• Path-induced homomorphisms. Show that HomotopyGroup.pi1EquivFundamentalGroup is a group isomorphism.
• Examples with 𝕊^n: π_n (𝕊^n) = ℤ, π_m (𝕊^n) trivial for m < n.
• Actions of π_1 on π_n.
• Lie algebra: ⁅π_(n+1), π_(m+1)⁆ contained in π_(n+m+1).

def Topology.«termI^_» : Lean.ParserDescr

I^N is notation (in the Topology namespace) for N → I, i.e. the unit cube indexed by a type N.

def Cube.boundary (N : Type u_1) : Set (N → ↑unitInterval)

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

@[reducible, inline]

abbrev Cube.splitAt {N : Type u_1} [DecidableEq N] (i : N) : (N → ↑unitInterval) ≃ₜ ↑unitInterval × ({ j : N // j ≠ i } → ↑unitInterval)

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

@[reducible, inline]

abbrev Cube.insertAt {N : Type u_1} [DecidableEq N] (i : N) : ↑unitInterval × ({ j : N // j ≠ i } → ↑unitInterval) ≃ₜ (N → ↑unitInterval)

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

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 ∈ boundary { j : N // j ≠ i }) : (insertAt i) (t₀, t) ∈ boundary N

@[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. Denoted as Ω, within the Topology.Homotopy namespace.

def Topology.Homotopy.termΩ : Lean.ParserDescr

The space of paths with both endpoints equal to a specified point x : X. Denoted as Ω, within the Topology.Homotopy namespace.

instance LoopSpace.inhabited (X : Type u_2) [TopologicalSpace X] (x : X) : Inhabited (Path x x)

def GenLoop (N : Type u_1) (X : Type u_2) [TopologicalSpace X] (x : X) : Set C(N → ↑unitInterval, 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.

def Topology.Homotopy.«termΩ^» : Lean.ParserDescr

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.

instance GenLoop.instFunLike {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : FunLike (↑(GenLoop N X x)) (N → ↑unitInterval) X

theorem GenLoop.ext {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f g : ↑(GenLoop N X x)) (H : ∀ (y : N → ↑unitInterval), f y = g y) : f = g

theorem GenLoop.ext_iff {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f g : ↑(GenLoop N X x)} : f = g ↔ ∀ (y : N → ↑unitInterval), f y = g y

@[simp]

theorem GenLoop.mk_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : C(N → ↑unitInterval, X)) (H : f ∈ GenLoop N X x) (y : N → ↑unitInterval) : ⟨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)) (N → ↑unitInterval) X

instance GenLoop.instContinuousEvalConst {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : ContinuousEvalConst (↑(GenLoop N X x)) (N → ↑unitInterval) X

def GenLoop.copy {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) (g : (N → ↑unitInterval) → 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.

theorem GenLoop.coe_copy {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) {g : (N → ↑unitInterval) → X} (h : g = ⇑f) : ⇑(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 : (N → ↑unitInterval) → X} (h : g = ⇑f) : 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 : N → ↑unitInterval) : y ∈ Cube.boundary N → f 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.

@[simp]

theorem GenLoop.const_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {t : N → ↑unitInterval} : const t = x

instance GenLoop.inhabited {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : Inhabited ↑(GenLoop N X x)

def GenLoop.Homotopic {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f g : ↑(GenLoop N X x)) : Prop

The "homotopic relative to boundary" relation between GenLoops.

theorem GenLoop.Homotopic.refl {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) : Homotopic f f

theorem GenLoop.Homotopic.symm {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f g : ↑(GenLoop N X x)} (H : Homotopic f g) : Homotopic g f

theorem GenLoop.Homotopic.trans {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f g h : ↑(GenLoop N X x)} (H0 : Homotopic f g) (H1 : Homotopic g h) : Homotopic f h

theorem GenLoop.Homotopic.equiv {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : Equivalence Homotopic

instance GenLoop.Homotopic.setoid {X : Type u_2} [TopologicalSpace X] (N : Type u_3) (x : X) : Setoid ↑(GenLoop N X x)

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)) const

Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus\{j\}} → X)$.

@[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) : ↑((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) : Continuous (toLoop i)

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)) const) : ↑(GenLoop N X x)

Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$.

@[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)) const) : ↑(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) : Continuous (fromLoop i)

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)) const) : toLoop i (fromLoop i p) = p

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)) 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.

@[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)) const) : (loopHomeo i).symm p = fromLoop i p

@[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)) : (loopHomeo i) p = toLoop i p

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} : ((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)) const} {t : N → ↑unitInterval} : (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(N → ↑unitInterval, X), C(↑unitInterval × ({ j : N // j ≠ i } → ↑unitInterval), X))

Composition with Cube.insertAt as a continuous map.

def GenLoop.homotopyTo {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p 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.

theorem GenLoop.homotopyTo_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p q : ↑(GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) (t : ↑unitInterval × ↑unitInterval) (tₙ : { j : N // j ≠ i } → ↑unitInterval) : ((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 q : ↑(GenLoop N X x)} : Homotopic p q → Path.Homotopic (toLoop i p) (toLoop i q)

def GenLoop.homotopyFrom {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p q : ↑(GenLoop N X x)} (H : Path.Homotopy (toLoop i p) (toLoop i q)) : C(↑unitInterval × (N → ↑unitInterval), X)

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.

@[simp]

theorem GenLoop.homotopyFrom_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) {p q : ↑(GenLoop N X x)} (H : Path.Homotopy (toLoop i p) (toLoop i q)) (a✝ : ↑unitInterval × (N → ↑unitInterval)) : (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 q : ↑(GenLoop N X x)} : Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

def GenLoop.transAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f g : ↑(GenLoop N X x)) : ↑(GenLoop N X x)

Concatenation of two GenLoops along the ith coordinate.

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.

theorem GenLoop.transAt_distrib {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i j : N} (h : i ≠ j) (a b c d : ↑(GenLoop N X x)) : transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

theorem GenLoop.fromLoop_trans_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} {p q : ↑(GenLoop N X x)} : fromLoop i (Path.trans (toLoop i p) (toLoop i q)) = transAt i p q

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)} : fromLoop i (Path.symm (toLoop i p)) = symmAt i p

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.

instance instInhabitedHomotopyGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : Inhabited (HomotopyGroup N X x)

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.

@[reducible, inline]

abbrev HomotopyGroup.Pi (n : ℕ) (X : Type u_3) [TopologicalSpace X] (x : X) : Type u_3

Homotopy group of finite index, denoted as π_n within the Topology namespace.

def Topology.termπ_ : Lean.ParserDescr

Homotopy group of finite index, denoted as π_n within the Topology namespace.

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.

def homotopyGroupEquivZerothHomotopyOfIsEmpty {X : Type u_2} [TopologicalSpace X] (N : Type u_3) (x : X) [IsEmpty N] : HomotopyGroup N X x ≃ ZerothHomotopy X

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

def HomotopyGroup.pi0EquivZerothHomotopy {X : Type u_2} [TopologicalSpace X] {x : X} : Pi 0 X x ≃ ZerothHomotopy X

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

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.

def homotopyGroupEquivFundamentalGroupOfUnique {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] : HomotopyGroup N X x ≃ FundamentalGroup 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.

def HomotopyGroup.pi1EquivFundamentalGroup {X : Type u_2} [TopologicalSpace X] {x : X} : Pi 1 X x ≃ FundamentalGroup X x

The first homotopy group at x is in bijection with the fundamental group.

instance HomotopyGroup.group {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [DecidableEq N] [Nonempty N] : Group (HomotopyGroup N X x)

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

@[reducible, inline]

abbrev HomotopyGroup.auxGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) : Group (HomotopyGroup N X x)

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.

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.auxGroup_indep {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i j : N) : auxGroup i = auxGroup j

theorem HomotopyGroup.transAt_indep {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] {i : N} (j : N) (f 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 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] : CommGroup (HomotopyGroup N X x)

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