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

Equations
Instances For
instance instGroupFundamentalGroup (X : Type u) [] (x : X) :
Equations
• = id inferInstance
instance instInhabitedFundamentalGroup (X : Type u) [] (x : X) :
Equations
• = id inferInstance
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

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
• = { hom := p, inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[reducible, inline]
abbrev FundamentalGroup.fromPath {X : TopCat} {x : X} (p : ) :

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

Equations
Instances For