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.

Equations

• Path.Homotopy.reflTransSymmAux x = if ↑x.2 ≤ 1 / 2 then ↑x.1 * 2 * ↑x.2 else ↑x.1 * (2 - 2 * ↑x.2)

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

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

• Path.Homotopy.reflSymmTrans p = (Path.Homotopy.reflTransSymm p.symm).cast ⋯ ⋯

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

Auxiliary function for trans_refl_reparam.

Equations

• Path.Homotopy.transReflReparamAux t = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

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₁) : p.trans (Path.refl x₁) = p.reparam (fun (t : ↑unitInterval) => ⟨Path.Homotopy.transReflReparamAux t, ⋯⟩) ⋯ ⋯ ⋯

def Path.Homotopy.transRefl {X : Type u} [TopologicalSpace X] {x₀ : 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

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

def Path.Homotopy.reflTrans {X : Type u} [TopologicalSpace X] {x₀ : 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

• Path.Homotopy.reflTrans p = (Path.Homotopy.transRefl p.symm).symm₂.cast ⋯ ⋯

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

Auxiliary function for trans_assoc_reparam.

Equations

• Path.Homotopy.transAssocReparamAux t = if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)

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₃) : (p.trans q).trans r = (p.trans (q.trans r)).reparam (fun (t : ↑unitInterval) => ⟨Path.Homotopy.transAssocReparamAux t, ⋯⟩) ⋯ ⋯ ⋯

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₃) : ((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.

theorem FundamentalGroupoid.ext_iff {X : Type u} (x : FundamentalGroupoid X) (y : FundamentalGroupoid X) : x = y ↔ x.as = y.as

theorem FundamentalGroupoid.ext {X : Type u} (x : FundamentalGroupoid X) (y : FundamentalGroupoid X) (as : x.as = y.as) : x = y

structure FundamentalGroupoid (X : Type u) : 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.

@[simp]

theorem FundamentalGroupoid.equiv_apply (X : Type u_1) (x : FundamentalGroupoid X) : (FundamentalGroupoid.equiv X) x = x.as

@[simp]

theorem FundamentalGroupoid.equiv_symm_apply_as (X : Type u_1) (x : X) : ((FundamentalGroupoid.equiv X).symm x).as = x

def FundamentalGroupoid.equiv (X : Type u_1) : FundamentalGroupoid X ≃ 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

• FundamentalGroupoid.equiv X = { toFun := fun (x : FundamentalGroupoid X) => x.as, invFun := fun (x : X) => { as := x }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FundamentalGroupoid.isEmpty_iff (X : Type u_1) : IsEmpty (FundamentalGroupoid X) ↔ IsEmpty X

instance FundamentalGroupoid.instIsEmpty (X : Type u_1) [IsEmpty X] : IsEmpty (FundamentalGroupoid X)

Equations

• ⋯ = ⋯

@[simp]

theorem FundamentalGroupoid.nonempty_iff (X : Type u_1) : Nonempty (FundamentalGroupoid X) ↔ Nonempty X

instance FundamentalGroupoid.instNonempty (X : Type u_1) [Nonempty X] : Nonempty (FundamentalGroupoid X)

Equations

• ⋯ = ⋯

@[simp]

theorem FundamentalGroupoid.subsingleton_iff (X : Type u_1) : Subsingleton (FundamentalGroupoid X) ↔ Subsingleton X

instance FundamentalGroupoid.instSubsingleton (X : Type u_1) [Subsingleton X] : Subsingleton (FundamentalGroupoid X)

Equations

• ⋯ = ⋯

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

Equations

• FundamentalGroupoid.instInhabited = { default := { as := default } }

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

Equations

• FundamentalGroupoid.instGroupoid = CategoryTheory.Groupoid.mk (fun {x y : FundamentalGroupoid X} (p : x ⟶ y) => Quotient.lift (fun (l : Path x.as y.as) => ⟦l.symm⟧) ⋯ p) ⋯ ⋯

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 = ⟦Path.refl x.as⟧

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

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

Equations

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

def FundamentalGroupoid.termπ : Lean.ParserDescr

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

Equations

• FundamentalGroupoid.termπ = Lean.ParserDescr.node `FundamentalGroupoid.termπ 1024 (Lean.ParserDescr.symbol "π")

def FundamentalGroupoid.termπₓ : Lean.ParserDescr

The fundamental groupoid of a topological space.

Equations

• FundamentalGroupoid.termπₓ = Lean.ParserDescr.node `FundamentalGroupoid.termπₓ 1024 (Lean.ParserDescr.symbol "πₓ")

def FundamentalGroupoid.termπₘ : Lean.ParserDescr

The functor between fundamental groupoids induced by a continuous map.

Equations

• FundamentalGroupoid.termπₘ = Lean.ParserDescr.node `FundamentalGroupoid.termπₘ 1024 (Lean.ParserDescr.symbol "πₘ")

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 = p.mapFn f

@[reducible, inline]

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

Equations

• FundamentalGroupoid.toTop x = x.as

@[reducible, inline]

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

Equations

• FundamentalGroupoid.fromTop x = { as := x }

@[reducible, inline]

abbrev FundamentalGroupoid.toPath {X : TopCat} {x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)} {x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj 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

• FundamentalGroupoid.toPath p = p

@[reducible, inline]

abbrev FundamentalGroupoid.fromPath {X : TopCat} {x₀ : ↑X} {x₁ : ↑X} (p : Path.Homotopic.Quotient x₀ x₁) : { 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

• FundamentalGroupoid.fromPath p = p