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, 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\}}$.

Equations

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

@[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\}}$.

Equations

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

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

• 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) : ⟨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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 = ⟨{ 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 : (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 = ⟨ContinuousMap.const (N → ↑unitInterval) 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)

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 = (↑f).HomotopicRel (↑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 := ⋯ }

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

• GenLoop.toLoop i p = { toFun := fun (t : ↑unitInterval) => ⟨((↑p).comp ↑(Cube.insertAt i)).curry t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

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

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

Equations

• GenLoop.fromLoop i p = ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp ↑(Cube.splitAt 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) = ({ 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 (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

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 = { toFun := GenLoop.toLoop i, invFun := GenLoop.fromLoop i, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

Equations

• GenLoop.cCompInsert i = { toFun := fun (f : C(N → ↑unitInterval, X)) => f.comp ↑(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 : (↑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

• GenLoop.homotopyTo i H = ({ toFun := ContinuousMap.curry, continuous_toFun := ⋯ }.comp ((GenLoop.cCompInsert i).comp H.curry)).uncurry

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

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.

@[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 = 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)} : 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, inline]

abbrev 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 = (homotopyGroupEquivFundamentalGroup (Classical.arbitrary N)).group

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

Equations

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

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

Equations

• HomotopyGroup.commGroup = EckmannHilton.commGroup ⋯ ⋯