Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup

Fundamental group of a space #

Given a topological space X and a basepoint x, the fundamental group is the automorphism group of x i.e. the group with elements being loops based at x (quotiented by homotopy equivalence).

def FundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) :

The fundamental group is the automorphism group (vertex group) of the basepoint in the fundamental groupoid.

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

    Get an isomorphism between the fundamental groups at two points given a path

    Equations
    Instances For

      The fundamental group of a path connected space is independent of the choice of basepoint.

      Equations
      Instances For
        @[reducible, inline]
        abbrev FundamentalGroup.toArrow {X : TopCat} {x : X} (p : FundamentalGroup (X) x) :
        { as := x } { as := x }

        An element of the fundamental group as an arrow in the fundamental groupoid.

        Equations
        • p.toArrow = p.hom
        Instances For
          @[reducible, inline]
          abbrev FundamentalGroup.toPath {X : TopCat} {x : X} (p : FundamentalGroup (X) x) :

          An element of the fundamental group as a quotient of homotopic paths.

          Equations
          • p.toPath = p.toArrow
          Instances For
            @[reducible, inline]
            abbrev FundamentalGroup.fromArrow {X : TopCat} {x : X} (p : { as := x } { as := x }) :

            An element of the fundamental group, constructed from an arrow in the fundamental groupoid.

            Equations
            Instances For
              @[reducible, inline]
              abbrev FundamentalGroup.fromPath {X : TopCat} {x : X} (p : Path.Homotopic.Quotient x x) :

              An element of the fundamental group, constructed from a quotient of homotopic paths.

              Equations
              Instances For