# mathlib3documentation

algebraic_topology.fundamental_groupoid.basic

# Fundamental groupoid 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, 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) :

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
Instances for fundamental_groupoid
@[protected, instance]
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 =

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

Equations
theorem fundamental_groupoid.map_eq {X Y : Top} {x₀ x₁ : X} (f : C(X, Y)) (p : x₁) :
@[reducible]

Help the typechecker by converting a point in a groupoid back to a point in the underlying topological space.

Equations
@[reducible]
def fundamental_groupoid.from_top {X : Top} (x : X) :

Help the typechecker by converting a point in a topological space to a point in the fundamental groupoid of that space

Equations
@[reducible]
def fundamental_groupoid.to_path {X : Top} {x₀ x₁ : } (p : x₀ x₁) :

Help the typechecker by converting an arrow in the fundamental groupoid of a topological space back to a path in that space (i.e., path.homotopic.quotient).

Equations
@[reducible]
def fundamental_groupoid.from_path {X : Top} {x₀ x₁ : X} (p : x₁) :
x₀ x₁

Help the typechecker by convering a path in a topological space to an arrow in the fundamental groupoid of that space.

Equations