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.

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

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

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

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

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

          Equations
          Instances For

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

              Equations
              • GenLoop.copy f g h = { toFun := g, continuous_toFun := },
              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.

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

                  The "homotopic relative to boundary" relation between GenLoops.

                  Equations
                  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)
                    Equations
                    @[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).toContinuousMap).curry 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
                    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 : N // j i } X x)) GenLoop.const) :
                      (GenLoop.fromLoop i p) = ({ toFun := Subtype.val, continuous_toFun := }.comp p.toContinuousMap).uncurry.comp (Cube.splitAt i).toContinuousMap
                      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).toContinuousMap,
                      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 : N // 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)) :
                        @[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) :
                        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
                        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 : 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 : NunitInterval} :
                          (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(NunitInterval, X), C(unitInterval × ({ j : N // j i }unitInterval), X))

                          Composition with Cube.insertAt as a continuous map.

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

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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.

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

                                    Equations
                                    Instances For
                                      instance instInhabitedHomotopyGroup {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} :
                                      Equations
                                      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
                                      Instances For
                                        @[reducible, inline]
                                        abbrev HomotopyGroup.Pi (n : ) (X : Type u_3) [TopologicalSpace X] (x : X) :
                                        Type u_3

                                        Homotopy group of finite index.

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

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

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

                                            Equations
                                            Instances For

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

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                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.

                                                  Equations
                                                  Instances For

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

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

                                                      Equations
                                                      @[reducible, inline]
                                                      abbrev 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.

                                                      Equations
                                                      Instances For
                                                        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.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] :

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

                                                        Equations