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_1) [TopologicalSpace X] (x : X) :
Type u_1

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

Equations
Instances For

    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 : Type u_1} [TopologicalSpace X] {x : X} (p : FundamentalGroup X x) :
        { as := x } { as := x }

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

        Equations
        Instances For
          @[reducible, inline]

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

          Equations
          Instances For
            @[reducible, inline]
            abbrev FundamentalGroup.fromArrow {X : Type u_1} [TopologicalSpace X] {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]

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

              Equations
              Instances For
                def FundamentalGroup.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) :

                The homomorphism between fundamental groups induced by a continuous map.

                Equations
                Instances For
                  @[simp]
                  theorem FundamentalGroup.map_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) (a✝ : { as := x } { as := x }) :
                  def FundamentalGroup.mapOfEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x : X} {y : Y} (h : f x = y) :

                  The homomorphism from π₁(X, x) to π₁(Y, y) induced by a continuous map f with f x = y.

                  Equations
                  Instances For
                    theorem FundamentalGroup.mapOfEq_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x : X} {y : Y} (h : f x = y) (p : Path x x) :
                    (mapOfEq f h) (fromPath p) = fromPath (p.map ).cast