mathlib documentation

topology.homotopy.fundamental_groupoid

Fundamental groupoid of a space #

Given a topological space X, we can define the fundamental groupoid of X to be the category with objects being points of X, and morphisms x ⟶ y being paths from x to y, quotiented by homotopy equivalence. With this, the fundamental group of X based at x is just the automorphism group of x.

Auxilliary function for refl_trans_symm

Equations
noncomputable def path.homotopy.refl_trans_symm {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :

For any path p from x₀ to x₁, we have a homotopy from the constant path based at x₀ to p.trans p.symm.

Equations
noncomputable def path.homotopy.refl_symm_trans {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :

For any path p from x₀ to x₁, we have a homotopy from the constant path based at x₁ to p.symm.trans p.

Equations

Auxilliary function for trans_refl_reparam

Equations
theorem path.homotopy.trans_refl_reparam {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :
noncomputable def path.homotopy.trans_refl {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :
(p.trans (path.refl x₁)).homotopy p

For any path p from x₀ to x₁, we have a homotopy from p.trans (path.refl x₁) to p.

Equations
noncomputable def path.homotopy.refl_trans {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :
((path.refl x₀).trans p).homotopy p

For any path p from x₀ to x₁, we have a homotopy from (path.refl x₀).trans p to p.

Equations

Auxilliary function for trans_assoc_reparam.

Equations
theorem path.homotopy.trans_assoc_reparam {X : Type u} [topological_space X] {x₀ x₁ x₂ x₃ : X} (p : path x₀ x₁) (q : path x₁ x₂) (r : path x₂ x₃) :
noncomputable def path.homotopy.trans_assoc {X : Type u} [topological_space X] {x₀ x₁ x₂ x₃ : X} (p : path x₀ x₁) (q : path x₁ x₂) (r : path x₂ x₃) :
((p.trans q).trans r).homotopy (p.trans (q.trans r))

For paths p q r, we have a homotopy from (p.trans q).trans r to p.trans (q.trans r).

Equations
def fundamental_groupoid (X : Type u) :
Type u

The fundamental groupoid of a space X is defined to be a type synonym for X, and we subsequently put a category_theory.groupoid structure on it.

Equations
@[protected, instance]
Equations
theorem fundamental_groupoid.comp_eq {X : Type u} [topological_space X] (x y z : fundamental_groupoid X) (p : x y) (q : y z) :

The functor sending a topological space X to its fundamental groupoid.

Equations