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.

Instances For
    @[reducible]
    def Cube.splitAt {N : Type u_1} [DecidableEq N] (i : N) :
    (NunitInterval) ≃ₜ unitInterval × ({ j // j i }unitInterval)

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

    Instances For
      @[reducible]
      def Cube.insertAt {N : Type u_1} [DecidableEq N] (i : N) :
      unitInterval × ({ j // j i }unitInterval) ≃ₜ (NunitInterval)

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

      Instances For
        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.

        Instances For
          instance LoopSpace.inhabited (X : Type u_2) [TopologicalSpace X] (x : X) :
          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.

          Instances For
            instance GenLoop.funLike {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
            FunLike (↑(GenLoop N X x)) (NunitInterval) 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 : 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) :
            { 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 : (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.

            Instances For
              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.

              Instances For
                @[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)
                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.

                Instances For
                  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)
                  @[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) :
                  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)$.

                  Instances For
                    theorem GenLoop.continuous_toLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
                    @[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) :
                    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$.

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

                      Instances For
                        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 : NunitInterval} :
                        ↑(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(NunitInterval, X), C(unitInterval × ({ j // j i }unitInterval), X))

                        Composition with Cube.insertAt as a continuous map.

                        Instances For
                          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)) :

                          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.

                          Instances For
                            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)} :
                            @[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 = ↑(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)) :

                            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.

                            Instances For
                              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.

                              Instances For
                                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.

                                Instances For
                                  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.

                                  Instances For
                                    instance instInhabitedHomotopyGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {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.

                                    Instances For
                                      @[reducible]
                                      def HomotopyGroup.Pi (n : ) (X : Type u_3) [TopologicalSpace X] (x : X) :
                                      Type u_3

                                      Homotopy group of finite index.

                                      Instances For
                                        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.

                                        Instances For

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

                                          Instances For

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

                                            Instances For
                                              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.

                                              Instances For

                                                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.

                                                Instances For

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

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

                                                    @[reducible]
                                                    def 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.

                                                    Instances For
                                                      theorem HomotopyGroup.isUnital_auxGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) :
                                                      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)) :
                                                      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)} :

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

                                                      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.