# Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

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

Auxiliary function for reflTransSymm.

Instances For
def Path.Homotopy.reflTransSymm {X : Type u} [] {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.

Instances For
def Path.Homotopy.reflSymmTrans {X : Type u} [] {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.

Instances For

Auxiliary function for trans_refl_reparam.

Instances For
theorem Path.Homotopy.trans_refl_reparam {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
Path.trans p () = Path.reparam p (fun t => { val := , property := }) (_ : Continuous fun x => { val := , property := }) (_ : (fun t => { val := , property := }) 0 = 0) (_ : (fun t => { val := , property := }) 1 = 1)
def Path.Homotopy.transRefl {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

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

Instances For
def Path.Homotopy.reflTrans {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :

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

Instances For

Auxiliary function for trans_assoc_reparam.

Instances For
theorem Path.Homotopy.trans_assoc_reparam {X : Type u} [] {x₀ : X} {x₁ : X} {x₂ : X} {x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
Path.trans () r = Path.reparam (Path.trans p ()) (fun t => { val := , property := }) (_ : Continuous fun x => { val := , property := }) (_ : (fun t => { val := , property := }) 0 = 0) (_ : (fun t => { val := , property := }) 1 = 1)
def Path.Homotopy.transAssoc {X : Type u} [] {x₀ : X} {x₁ : X} {x₂ : X} {x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :

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

Instances For
@[reducible]

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

Instances For
theorem FundamentalGroupoid.comp_eq {X : Type u} [] (x : ) (y : ) (z : ) (p : x y) (q : y z) :

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

Instances For
Instances For
Instances For
Instances For
theorem FundamentalGroupoid.map_eq {X : TopCat} {Y : TopCat} {x₀ : X} {x₁ : X} (f : C(X, Y)) (p : ) :
@[reducible]
def FundamentalGroupoid.toTop {X : TopCat} (x : ) :
X

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

Instances For
@[reducible]
def FundamentalGroupoid.fromTop {X : TopCat} (x : X) :

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

Instances For
@[reducible]
def FundamentalGroupoid.toPath {X : TopCat} {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).

Instances For
@[reducible]
def FundamentalGroupoid.fromPath {X : TopCat} {x₀ : X} {x₁ : X} (p : ) :
x₀ x₁

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

Instances For