mathlib3 documentation

algebraic_topology.fundamental_groupoid.fundamental_group

Fundamental group of a space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
noncomputable def fundamental_group.inhabited (X : Type u) [topological_space X] (x : X) :
@[protected, instance]
noncomputable def fundamental_group.group (X : Type u) [topological_space X] (x : X) :
def fundamental_group (X : Type u) [topological_space X] (x : X) :

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

Equations
Instances for fundamental_group
noncomputable def fundamental_group.fundamental_group_mul_equiv_of_path {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :

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

Equations

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

Equations
@[reducible]
noncomputable def fundamental_group.to_arrow {X : Top} {x : X} (p : fundamental_group X x) :
x x

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

@[reducible]
noncomputable def fundamental_group.to_path {X : Top} {x : X} (p : fundamental_group X x) :

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

@[reducible]
noncomputable def fundamental_group.from_arrow {X : Top} {x : X} (p : x x) :

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

@[reducible]
noncomputable def fundamental_group.from_path {X : Top} {x : X} (p : path.homotopic.quotient x x) :

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