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.

def Path.Homotopy.reflTransSymmAux (x : ↑unitInterval × ↑unitInterval) : ℝ

Auxiliary function for reflTransSymm.

theorem Path.Homotopy.continuous_reflTransSymmAux : Continuous Path.Homotopy.reflTransSymmAux

theorem Path.Homotopy.reflTransSymmAux_mem_I (x : ↑unitInterval × ↑unitInterval) : Path.Homotopy.reflTransSymmAux x ∈ unitInterval

def Path.Homotopy.reflTransSymm {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) : Path.Homotopy (Path.refl x₀) (Path.trans p (Path.symm p))

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

def Path.Homotopy.reflSymmTrans {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) : Path.Homotopy (Path.refl x₁) (Path.trans (Path.symm p) 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.

def Path.Homotopy.transReflReparamAux (t : ↑unitInterval) : ℝ

Auxiliary function for trans_refl_reparam.

theorem Path.Homotopy.continuous_transReflReparamAux : Continuous Path.Homotopy.transReflReparamAux

theorem Path.Homotopy.transReflReparamAux_mem_I (t : ↑unitInterval) : Path.Homotopy.transReflReparamAux t ∈ unitInterval

theorem Path.Homotopy.transReflReparamAux_zero : Path.Homotopy.transReflReparamAux 0 = 0

theorem Path.Homotopy.transReflReparamAux_one : Path.Homotopy.transReflReparamAux 1 = 1

theorem Path.Homotopy.trans_refl_reparam {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) : Path.trans p (Path.refl x₁) = Path.reparam p (fun t => { val := Path.Homotopy.transReflReparamAux t, property := (_ : Path.Homotopy.transReflReparamAux t ∈ unitInterval) }) (_ : Continuous fun x => { val := Path.Homotopy.transReflReparamAux x, property := (_ : Path.Homotopy.transReflReparamAux x ∈ unitInterval) }) (_ : (fun t => { val := Path.Homotopy.transReflReparamAux t, property := (_ : Path.Homotopy.transReflReparamAux t ∈ unitInterval) }) 0 = 0) (_ : (fun t => { val := Path.Homotopy.transReflReparamAux t, property := (_ : Path.Homotopy.transReflReparamAux t ∈ unitInterval) }) 1 = 1)

def Path.Homotopy.transRefl {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) : Path.Homotopy (Path.trans p (Path.refl x₁)) p

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

def Path.Homotopy.reflTrans {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) : Path.Homotopy (Path.trans (Path.refl x₀) p) p

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

def Path.Homotopy.transAssocReparamAux (t : ↑unitInterval) : ℝ

Auxiliary function for trans_assoc_reparam.

theorem Path.Homotopy.continuous_transAssocReparamAux : Continuous Path.Homotopy.transAssocReparamAux

theorem Path.Homotopy.transAssocReparamAux_mem_I (t : ↑unitInterval) : Path.Homotopy.transAssocReparamAux t ∈ unitInterval

theorem Path.Homotopy.transAssocReparamAux_zero : Path.Homotopy.transAssocReparamAux 0 = 0

theorem Path.Homotopy.transAssocReparamAux_one : Path.Homotopy.transAssocReparamAux 1 = 1

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

def Path.Homotopy.transAssoc {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) : Path.Homotopy (Path.trans (Path.trans p q) r) (Path.trans p (Path.trans q r))

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

@[reducible]

def FundamentalGroupoid (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 CategoryTheory.Groupoid structure on it.

instance FundamentalGroupoid.instInhabitedFundamentalGroupoid {X : Type u} [h : Inhabited X] : Inhabited (FundamentalGroupoid X)

instance FundamentalGroupoid.instGroupoidFundamentalGroupoid {X : Type u} [TopologicalSpace X] : CategoryTheory.Groupoid (FundamentalGroupoid X)

theorem FundamentalGroupoid.comp_eq {X : Type u} [TopologicalSpace X] (x : FundamentalGroupoid X) (y : FundamentalGroupoid X) (z : FundamentalGroupoid X) (p : x ⟶ y) (q : y ⟶ z) : CategoryTheory.CategoryStruct.comp p q = Path.Homotopic.Quotient.comp p q

theorem FundamentalGroupoid.id_eq_path_refl {X : Type u} [TopologicalSpace X] (x : FundamentalGroupoid X) : CategoryTheory.CategoryStruct.id x = Quotient.mk (Path.Homotopic.setoid x x) (Path.refl x)

def FundamentalGroupoid.fundamentalGroupoidFunctor : CategoryTheory.Functor TopCat CategoryTheory.Grpd

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

def FundamentalGroupoid.termπ : Lean.ParserDescr

def FundamentalGroupoid.termπₓ : Lean.ParserDescr

def FundamentalGroupoid.termπₘ : Lean.ParserDescr

theorem FundamentalGroupoid.map_eq {X : TopCat} {Y : TopCat} {x₀ : ↑X} {x₁ : ↑X} (f : C(↑X, ↑Y)) (p : Path.Homotopic.Quotient x₀ x₁) : (FundamentalGroupoid.fundamentalGroupoidFunctor.map f).map p = Path.Homotopic.Quotient.mapFn p f

@[reducible]

def FundamentalGroupoid.toTop {X : TopCat} (x : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)) : ↑X

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

@[reducible]

def FundamentalGroupoid.fromTop {X : TopCat} (x : ↑X) : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)

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

@[reducible]

def FundamentalGroupoid.toPath {X : TopCat} {x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)} {x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)} (p : x₀ ⟶ x₁) : Path.Homotopic.Quotient 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).

@[reducible]

def FundamentalGroupoid.fromPath {X : TopCat} {x₀ : ↑X} {x₁ : ↑X} (p : Path.Homotopic.Quotient x₀ x₁) : x₀ ⟶ x₁

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