Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Fundamental groupoid of a space #

Given a topological space X, we can define the fundamental groupoid of X to be the category with objects being points of X, and morphisms x ⟶ y being paths from x to y, quotiented by homotopy equivalence. With this, the fundamental group of X based at x is just the automorphism group of x.

Auxiliary function for reflTransSymm.

Instances For
    def Path.Homotopy.reflTransSymm {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

    For any path p from x₀ to x₁, we have a homotopy from the constant path based at x₀ to p.trans p.symm.

    Instances For
      def Path.Homotopy.reflSymmTrans {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

      For any path p from x₀ to x₁, we have a homotopy from the constant path based at x₁ to p.symm.trans p.

      Instances For

        Auxiliary function for trans_refl_reparam.

        Instances For
          theorem Path.Homotopy.trans_refl_reparam {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
          def Path.Homotopy.transRefl {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

          For any path p from x₀ to x₁, we have a homotopy from p.trans (Path.refl x₁) to p.

          Instances For
            def Path.Homotopy.reflTrans {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

            For any path p from x₀ to x₁, we have a homotopy from (Path.refl x₀).trans p to p.

            Instances For

              Auxiliary function for trans_assoc_reparam.

              Instances For
                theorem Path.Homotopy.trans_assoc_reparam {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
                def Path.Homotopy.transAssoc {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :

                For paths p q r, we have a homotopy from (p.trans q).trans r to p.trans (q.trans r).

                Instances For
                  @[reducible]

                  The fundamental groupoid of a space X is defined to be a type synonym for X, and we subsequently put a CategoryTheory.Groupoid structure on it.

                  Instances For

                    The functor sending a topological space X to its fundamental groupoid.

                    Instances For
                      theorem FundamentalGroupoid.map_eq {X : TopCat} {Y : TopCat} {x₀ : X} {x₁ : X} (f : C(X, Y)) (p : Path.Homotopic.Quotient x₀ x₁) :
                      @[reducible]

                      Help the typechecker by converting a point in a groupoid back to a point in the underlying topological space.

                      Instances For
                        @[reducible]

                        Help the typechecker by converting a point in a topological space to a point in the fundamental groupoid of that space.

                        Instances For
                          @[reducible]

                          Help the typechecker by converting an arrow in the fundamental groupoid of a topological space back to a path in that space (i.e., Path.Homotopic.Quotient).

                          Instances For
                            @[reducible]
                            def FundamentalGroupoid.fromPath {X : TopCat} {x₀ : X} {x₁ : X} (p : Path.Homotopic.Quotient x₀ x₁) :
                            x₀ x₁

                            Help the typechecker by converting a path in a topological space to an arrow in the fundamental groupoid of that space.

                            Instances For