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

Equations
• = if x.2 1 / 2 then x.1 * 2 * x.2 else x.1 * (2 - 2 * x.2)
Instances For
def Path.Homotopy.reflTransSymm {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
().Homotopy (p.trans p.symm)

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
• One or more equations did not get rendered due to their size.
Instances For
def Path.Homotopy.reflSymmTrans {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
().Homotopy (p.symm.trans p)

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
• = ().cast
Instances For

Auxiliary function for trans_refl_reparam.

Equations
• = if t 1 / 2 then 2 * t else 1
Instances For
theorem Path.Homotopy.trans_refl_reparam {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
p.trans () = p.reparam (fun (t : ) => )
def Path.Homotopy.transRefl {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
(p.trans ()).Homotopy p

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Path.Homotopy.reflTrans {X : Type u} [] {x₀ : X} {x₁ : X} (p : Path x₀ 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
Instances For

Auxiliary function for trans_assoc_reparam.

Equations
• = if t 1 / 4 then 2 * t else if t 1 / 2 then t + 1 / 4 else 1 / 2 * (t + 1)
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₃) :
(p.trans q).trans r = (p.trans (q.trans r)).reparam (fun (t : ) => )
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₃) :
((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
• One or more equations did not get rendered due to their size.
Instances For
theorem FundamentalGroupoid.ext_iff {X : Type u} (x : ) (y : ) :
x = y x.as = y.as
theorem FundamentalGroupoid.ext {X : Type u} (x : ) (y : ) (as : x.as = y.as) :
x = y
structure FundamentalGroupoid (X : Type u) :

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

• as : X

View a term of FundamentalGroupoid X as a term of X.

Instances For
@[simp]
theorem FundamentalGroupoid.equiv_apply (X : Type u_1) (x : ) :
= x.as
@[simp]
theorem FundamentalGroupoid.equiv_symm_apply_as (X : Type u_1) (x : X) :
(.symm x).as = x

The equivalence between X and the underlying type of its fundamental groupoid. This is useful for transferring constructions (instances, etc.) from X to πₓ X.

Equations
• = { toFun := fun (x : ) => x.as, invFun := fun (x : X) => { as := x }, left_inv := , right_inv := }
Instances For
@[simp]
instance FundamentalGroupoid.instIsEmpty (X : Type u_1) [] :
Equations
• =
@[simp]
instance FundamentalGroupoid.instNonempty (X : Type u_1) [] :
Equations
• =
Equations
• =
Equations
• FundamentalGroupoid.instInhabited = { default := { as := default } }
Equations
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
Instances For

The fundamental groupoid of a topological space.

Equations
Instances For

The functor between fundamental groupoids induced by a continuous map.

Equations
Instances For
theorem FundamentalGroupoid.map_eq {X : TopCat} {Y : TopCat} {x₀ : X} {x₁ : X} (f : C(X, Y)) (p : ) :
.map p = p.mapFn f
@[reducible, inline]
abbrev 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.

Equations
Instances For
@[reducible, inline]
abbrev 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.

Equations
• = { as := x }
Instances For
@[reducible, inline]
abbrev FundamentalGroupoid.toPath {X : TopCat} {x₀ : } {x₁ : } (p : x₀ x₁) :
Path.Homotopic.Quotient x₀.as x₁.as

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
Instances For
@[reducible, inline]
abbrev FundamentalGroupoid.fromPath {X : TopCat} {x₀ : X} {x₁ : X} (p : ) :
{ as := x₀ } { as := x₁ }

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

Equations
Instances For