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

Equations

• Topology.«termI^_» = Lean.ParserDescr.node `Topology.termI^_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "I^") (Lean.ParserDescr.cat `term 0))

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.

Equations

• Cube.boundary N = {y : N → ↑unitInterval | ∃ (i : N), y i = 0 ∨ y i = 1}

@[reducible]

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

Equations

• Cube.splitAt i = Homeomorph.funSplitAt (↑unitInterval) i

@[reducible]

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

Equations

• Cube.insertAt i = Homeomorph.symm (Homeomorph.funSplitAt (↑unitInterval) i)

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

Equations

• LoopSpace X x = Path x x

def Topology.Homotopy.termΩ : Lean.ParserDescr

Equations

• Topology.Homotopy.termΩ = Lean.ParserDescr.node `Topology.Homotopy.termΩ 1024 (Lean.ParserDescr.symbol "Ω")

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

Equations

• LoopSpace.inhabited X x = { default := Path.refl 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.

Equations

• GenLoop N X x = {p : C(N → ↑unitInterval, X) | ∀ y ∈ Cube.boundary N, p y = x}

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.

Equations

• Topology.Homotopy.«termΩ^» = Lean.ParserDescr.node `Topology.Homotopy.termΩ^ 1024 (Lean.ParserDescr.symbol "Ω^")

instance GenLoop.instFunLike {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} : FunLike (↑(GenLoop N X x)) (N → ↑unitInterval) 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 : 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.

Equations

• GenLoop.copy f g h = { val := { toFun := g, continuous_toFun := ⋯ }, property := ⋯ }

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.

Equations

• GenLoop.const = { val := ContinuousMap.const (N → ↑unitInterval) x, property := ⋯ }

@[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)

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

The "homotopic relative to boundary" relation between GenLoops.

Equations

• GenLoop.Homotopic f g = ContinuousMap.HomotopicRel (↑f) (↑g) (Cube.boundary N)

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)

Equations

• GenLoop.Homotopic.setoid N x = { r := GenLoop.Homotopic, iseqv := ⋯ }

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

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

Equations

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

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 : N // j ≠ i } X x)) GenLoop.const) : ↑(GenLoop.fromLoop i p) = ContinuousMap.comp (ContinuousMap.uncurry (ContinuousMap.comp { toFun := Subtype.val, continuous_toFun := ⋯ } 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 : N // 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$.

Equations

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

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 : N // j ≠ i } X x)) GenLoop.const) : GenLoop.toLoop i (GenLoop.fromLoop i p) = 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

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

• GenLoop.loopHomeo i = { toEquiv := { toFun := GenLoop.toLoop i, invFun := GenLoop.fromLoop i, left_inv := ⋯, right_inv := ⋯ }, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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 : N → ↑unitInterval} : (GenLoop.fromLoop i p) t = (p (t i)) ((Cube.splitAt i) t).2

@[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 : N // j ≠ i } → ↑unitInterval), X))

Composition with Cube.insertAt as a continuous map.

Equations

• GenLoop.cCompInsert i = { toFun := fun (f : C(N → ↑unitInterval, X)) => ContinuousMap.comp f (Homeomorph.toContinuousMap (Cube.insertAt i)), continuous_toFun := ⋯ }

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

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

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 : 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)} : 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.1, a.2 i)) fun (j : { j : N // ¬j = i }) => a.2 ↑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.

Equations

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

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.

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

• GenLoop.symmAt i f = GenLoop.copy (GenLoop.fromLoop i (Path.symm (GenLoop.toLoop i f))) (fun (t : N → ↑unitInterval) => f fun (j : N) => if j = i then unitInterval.symm (t i) else t j) ⋯

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.

Equations

• HomotopyGroup N X x = Quotient (GenLoop.Homotopic.setoid N x)

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

Equations

• instInhabitedHomotopyGroup = inferInstanceAs (Inhabited (Quotient (GenLoop.Homotopic.setoid N 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.

Equations

• homotopyGroupEquivFundamentalGroup i = (Quotient.congr (GenLoop.loopHomeo i).toEquiv ⋯).trans (CategoryTheory.Groupoid.isoEquivHom { as := GenLoop.const } { as := GenLoop.const }).symm

@[reducible]

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

Homotopy group of finite index.

Equations

• HomotopyGroup.Pi n X x = HomotopyGroup (Fin n) X x

def Topology.termπ_ : Lean.ParserDescr

Equations

• Topology.termπ_ = Lean.ParserDescr.node `Topology.termπ_ 1024 (Lean.ParserDescr.symbol "π_")

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.

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.

Equations

• homotopyGroupEquivZerothHomotopyOfIsEmpty N x = Quotient.congr (genLoopHomeoOfIsEmpty N x).toEquiv ⋯

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.

Equations

• HomotopyGroup.pi0EquivZerothHomotopy = homotopyGroupEquivZerothHomotopyOfIsEmpty (Fin 0) x

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.

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.

Equations

• homotopyGroupEquivFundamentalGroupOfUnique N = (Quotient.congr (genLoopEquivOfUnique N) ⋯).trans (CategoryTheory.Groupoid.isoEquivHom { as := x } { as := x }).symm

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.

Equations

• HomotopyGroup.pi1EquivFundamentalGroup = homotopyGroupEquivFundamentalGroupOfUnique (Fin 1)

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

Equations

• HomotopyGroup.group N = Equiv.group (homotopyGroupEquivFundamentalGroup (Classical.arbitrary N))

@[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.

Equations

• HomotopyGroup.auxGroup i = Equiv.group (homotopyGroupEquivFundamentalGroup i)

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 : 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)) : ⟦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 (x_1 x_2 : HomotopyGroup N X x) => x_1 * x_2) ⟦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.

Equations

• HomotopyGroup.commGroup = let h := ⋯; EckmannHilton.commGroup ⋯ ⋯