# 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) [] (x : X) :

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

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

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

Instances For

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

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

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

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

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

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

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

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

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

Instances For