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

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

Equations

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

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₁) : Path.trans p (Path.refl x₁) = Path.reparam p (fun (t : ↑unitInterval) => { val := Path.Homotopy.transReflReparamAux t, property := (_ : Path.Homotopy.transReflReparamAux t ∈ unitInterval) }) (_ : Continuous fun (x : ↑unitInterval) => { val := Path.Homotopy.transReflReparamAux x, property := (_ : Path.Homotopy.transReflReparamAux x ∈ unitInterval) }) (_ : (fun (t : ↑unitInterval) => { val := Path.Homotopy.transReflReparamAux t, property := (_ : Path.Homotopy.transReflReparamAux t ∈ unitInterval) }) 0 = 0) (_ : (fun (t : ↑unitInterval) => { 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.

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

Equations

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

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₃) : Path.trans (Path.trans p q) r = Path.reparam (Path.trans p (Path.trans q r)) (fun (t : ↑unitInterval) => { val := Path.Homotopy.transAssocReparamAux t, property := (_ : Path.Homotopy.transAssocReparamAux t ∈ unitInterval) }) (_ : Continuous fun (x : ↑unitInterval) => { val := Path.Homotopy.transAssocReparamAux x, property := (_ : Path.Homotopy.transAssocReparamAux x ∈ unitInterval) }) (_ : (fun (t : ↑unitInterval) => { val := Path.Homotopy.transAssocReparamAux t, property := (_ : Path.Homotopy.transAssocReparamAux t ∈ unitInterval) }) 0 = 0) (_ : (fun (t : ↑unitInterval) => { 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).

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

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

@[simp]

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

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

Equations

• (_ : IsEmpty (FundamentalGroupoid X)) = (_ : IsEmpty (FundamentalGroupoid X))

@[simp]

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

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

Equations

• (_ : Nonempty (FundamentalGroupoid X)) = (_ : Nonempty (FundamentalGroupoid X))

@[simp]

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

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

Equations

• (_ : Subsingleton (FundamentalGroupoid X)) = (_ : Subsingleton (FundamentalGroupoid X))

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

Equations

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

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

Equations

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

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.toPrefunctor.map f).toPrefunctor.map p = Path.Homotopic.Quotient.mapFn p f

@[reducible]

def FundamentalGroupoid.toTop {X : TopCat} (x : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.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]

def FundamentalGroupoid.fromTop {X : TopCat} (x : ↑X) : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.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]

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

def 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