# mathlibdocumentation

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.

noncomputable def path.homotopy.refl_trans_symm_aux  :

Auxilliary function for refl_trans_symm

Equations
@[continuity]
noncomputable def path.homotopy.refl_trans_symm {X : Type u} {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} {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
• = path.homotopy.refl_symm_trans._proof_1 _

Auxilliary function for trans_refl_reparam

Equations
@[continuity]
theorem path.homotopy.trans_refl_reparam {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁) :
p.trans (path.refl x₁) = p.reparam (λ (t : unit_interval), _ _ _
noncomputable def path.homotopy.trans_refl {X : Type u} {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
• = (λ (t : unit_interval), path.homotopy.trans_refl._proof_4 path.homotopy.trans_refl._proof_5 path.homotopy.trans_refl._proof_6).cast _ _).symm
noncomputable def path.homotopy.refl_trans {X : Type u} {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
@[continuity]
theorem path.homotopy.trans_assoc_reparam {X : Type u} {x₀ x₁ x₂ x₃ : X} (p : path x₀ x₁) (q : path x₁ x₂) (r : path x₂ x₃) :
(p.trans q).trans r = (p.trans (q.trans r)).reparam (λ (t : unit_interval), _ _ _
noncomputable def path.homotopy.trans_assoc {X : Type u} {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]
def fundamental_groupoid.inhabited {X : Type u} [h : inhabited X] :
Equations
@[protected, instance]
noncomputable def fundamental_groupoid.category_theory.groupoid {X : Type u}  :
Equations
theorem fundamental_groupoid.comp_eq {X : Type u} (x y z : fundamental_groupoid X) (p : x y) (q : y z) :
p q = q

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

Equations