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

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]

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

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

@[reducible]

def Cube.insertAt {N : Type u_1} [DecidableEq N] (i : N) : ↑unitInterval × ({ j // 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 // j ≠ i } → ↑unitInterval} (H : (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ Cube.boundary { j // j ≠ i }) : ↑(Cube.insertAt i) (t₀, t) ∈ Cube.boundary N

@[reducible]

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

def Topology.Homotopy.termΩ : Lean.ParserDescr

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

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

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 : N → ↑unitInterval), ↑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(N → ↑unitInterval, X)) (H : f ∈ GenLoop N X x) (y : N → ↑unitInterval) : ↑{ val := f, property := H } y = ↑f y

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) : ↑(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 : (N → ↑unitInterval) → 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 : 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} : ↑GenLoop.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 : ↑(GenLoop N X x)) (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)) : GenLoop.Homotopic f f

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) : GenLoop.Homotopic g f

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) : GenLoop.Homotopic f 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)

@[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) = ↑(ContinuousMap.curry (ContinuousMap.comp (↑p) (Homeomorph.toContinuousMap (Cube.insertAt i)))) t

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 // j ≠ i } X x)) GenLoop.const

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

theorem GenLoop.continuous_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) : Continuous (GenLoop.toLoop i)

@[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 // j ≠ i } X x)) GenLoop.const) : ↑(GenLoop.fromLoop i p) = ContinuousMap.comp (ContinuousMap.uncurry (ContinuousMap.comp (ContinuousMap.mk Subtype.val) p.toContinuousMap)) (Homeomorph.toContinuousMap (Cube.splitAt i))

def GenLoop.fromLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const) : ↑(GenLoop N X x)

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

theorem GenLoop.continuous_fromLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) : Continuous (GenLoop.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 // j ≠ i } X x)) GenLoop.const) : GenLoop.toLoop i (GenLoop.fromLoop i p) = p

@[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 // j ≠ i } X x)) GenLoop.const) : ↑(Homeomorph.symm (GenLoop.loopHomeo i)) p = GenLoop.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)) : ↑(GenLoop.loopHomeo i) p = GenLoop.toLoop i 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 // 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.

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 // 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 // j ≠ i } X x)) GenLoop.const} {t : N → ↑unitInterval} : ↑(GenLoop.fromLoop i p) t = ↑(↑p (t i)) (↑(Cube.splitAt i) t).snd

@[reducible]

def GenLoop.cCompInsert {N : Type u_1} {X : Type u_2} [TopologicalSpace X] [DecidableEq N] (i : N) : C(C(N → ↑unitInterval, X), C(↑unitInterval × ({ j // 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 : ↑(GenLoop N X x)} {q : ↑(GenLoop N X x)} (H : ContinuousMap.HomotopyRel (↑p) (↑q) (Cube.boundary N)) : C(↑unitInterval × ↑unitInterval, C({ j // 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 : ↑(GenLoop N X x)} {q : ↑(GenLoop N X x)} (H : ContinuousMap.HomotopyRel (↑p) (↑q) (Cube.boundary N)) (t : ↑unitInterval × ↑unitInterval) (tₙ : { j // j ≠ i } → ↑unitInterval) : ↑(↑(GenLoop.homotopyTo i H) t) tₙ = ↑H (t.fst, ↑(Cube.insertAt i) (t.snd, 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)} : GenLoop.Homotopic p q → Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q)

@[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 × (N → ↑unitInterval)), ↑(GenLoop.homotopyFrom i H) a = ↑↑(↑H (a.fst, Prod.snd a i)) fun j => Prod.snd a ↑j

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

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)} : Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q) → GenLoop.Homotopic p q

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.

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 : 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)) : GenLoop.transAt i (GenLoop.transAt j a b) (GenLoop.transAt j c d) = GenLoop.transAt j (GenLoop.transAt i a c) (GenLoop.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 : ↑(GenLoop N X x)} {q : ↑(GenLoop N X x)} : GenLoop.fromLoop i (Path.trans (GenLoop.toLoop i p) (GenLoop.toLoop i q)) = GenLoop.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)} : GenLoop.fromLoop i (Path.symm (GenLoop.toLoop i p)) = GenLoop.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 // j ≠ i } X x)) GenLoop.const

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

@[reducible]

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

Homotopy group of finite index.

def Topology.termπ_ : Lean.ParserDescr

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} : HomotopyGroup.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} : HomotopyGroup.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]

def 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 (Quotient.mk (GenLoop.Homotopic.setoid N x) GenLoop.const)

theorem HomotopyGroup.auxGroup_indep {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (j : N) : HomotopyGroup.auxGroup i = HomotopyGroup.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 : ↑(GenLoop N X x)) (g : ↑(GenLoop N X x)) : Quotient.mk (GenLoop.Homotopic.setoid N x) (GenLoop.transAt i f g) = Quotient.mk (GenLoop.Homotopic.setoid N x) (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)) : Quotient.mk (GenLoop.Homotopic.setoid N x) (GenLoop.symmAt i f) = Quotient.mk (GenLoop.Homotopic.setoid N x) (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 = Quotient.mk (GenLoop.Homotopic.setoid N x) 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 x x_1 => x * x_1) (Quotient.mk (GenLoop.Homotopic.setoid N x) p) (Quotient.mk (GenLoop.Homotopic.setoid N x) q) = Quotient.mk (GenLoop.Homotopic.setoid N x) (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)} : (Quotient.mk (GenLoop.Homotopic.setoid N x) p)⁻¹ = Quotient.mk (GenLoop.Homotopic.setoid N x) (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.