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

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

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

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

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

Equations
source
noncomputable def fundamental_group.fundamental_group_mul_equiv_of_path_connected {X : Type u} [topological_space X] (x₀ x₁ : X) [path_connected_space X] :
fundamental_group X x₀ ≃* fundamental_group X x₁

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

Equations
source
@[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.

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

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

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

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

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

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