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.

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

Auxiliary function for reflTransSymm.

theorem Path.Homotopy.continuous_reflTransSymmAux : Continuous reflTransSymmAux

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

noncomputable def Path.Homotopy.reflTransSymm {X : Type u_1} [TopologicalSpace 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.

noncomputable def Path.Homotopy.reflSymmTrans {X : Type u_1} [TopologicalSpace 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.

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

Auxiliary function for trans_refl_reparam.

theorem Path.Homotopy.continuous_transReflReparamAux : Continuous transReflReparamAux

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

theorem Path.Homotopy.transReflReparamAux_zero : transReflReparamAux 0 = 0

theorem Path.Homotopy.transReflReparamAux_one : transReflReparamAux 1 = 1

theorem Path.Homotopy.trans_refl_reparam {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : p.trans (Path.refl x₁) = p.reparam (fun (t : ↑unitInterval) => ⟨transReflReparamAux t, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯

noncomputable def Path.Homotopy.transRefl {X : Type u_1} [TopologicalSpace 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.

noncomputable def Path.Homotopy.reflTrans {X : Type u_1} [TopologicalSpace 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.

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

Auxiliary function for trans_assoc_reparam.

theorem Path.Homotopy.continuous_transAssocReparamAux : Continuous transAssocReparamAux

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

theorem Path.Homotopy.transAssocReparamAux_zero : transAssocReparamAux 0 = 0

theorem Path.Homotopy.transAssocReparamAux_one : transAssocReparamAux 1 = 1

theorem Path.Homotopy.trans_assoc_reparam {X : Type u_1} [TopologicalSpace 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) => ⟨transAssocReparamAux t, ⋯⟩) trans_assoc_reparam._proof_1 ⋯ ⋯

noncomputable def Path.Homotopy.transAssoc {X : Type u_1} [TopologicalSpace 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).

theorem Path.Homotopic.refl_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : ((Path.refl x₀).trans p).Homotopic p

theorem Path.Homotopic.trans_refl {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : (p.trans (Path.refl x₁)).Homotopic p

theorem Path.Homotopic.trans_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : (p.trans p.symm).Homotopic (Path.refl x₀)

theorem Path.Homotopic.symm_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : (p.symm.trans p).Homotopic (Path.refl x₁)

theorem Path.Homotopic.trans_assoc {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) : ((p.trans q).trans r).Homotopic (p.trans (q.trans r))

@[simp]

theorem Path.Homotopic.Quotient.refl_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Homotopic.Quotient x₀ x₁) : (refl x₀).trans γ = γ

@[simp]

theorem Path.Homotopic.Quotient.trans_refl {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Homotopic.Quotient x₀ x₁) : γ.trans (refl x₁) = γ

@[simp]

theorem Path.Homotopic.Quotient.trans_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Homotopic.Quotient x₀ x₁) : γ.trans γ.symm = refl x₀

@[simp]

theorem Path.Homotopic.Quotient.symm_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Homotopic.Quotient x₀ x₁) : γ.symm.trans γ = refl x₁

@[simp]

theorem Path.Homotopic.Quotient.trans_assoc {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (γ₀ : Homotopic.Quotient x₀ x₁) (γ₁ : Homotopic.Quotient x₁ x₂) (γ₂ : Homotopic.Quotient x₂ x₃) : (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)

structure FundamentalGroupoid (X : Type u_3) : Type u_3

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.

theorem FundamentalGroupoid.ext_iff {X : Type u_3} {x y : FundamentalGroupoid X} : x = y ↔ x.as = y.as

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

theorem FundamentalGroupoid.id_eq_path_refl {X : Type u_1} [TopologicalSpace X] (x : FundamentalGroupoid X) : CategoryTheory.CategoryStruct.id x = ⟦Path.refl x.as⟧

def FundamentalGroupoid.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : CategoryTheory.Functor (FundamentalGroupoid X) (FundamentalGroupoid Y)

The functor on fundamental groupoid induced by a continuous map.

@[simp]

theorem FundamentalGroupoid.map_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {X✝ Y✝ : FundamentalGroupoid X} (p : X✝ ⟶ Y✝) : (map f).map p = Path.Homotopic.Quotient.map p f

@[simp]

theorem FundamentalGroupoid.map_obj_as {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : FundamentalGroupoid X) : ((map f).obj x).as = f x.as

@[simp]

theorem FundamentalGroupoid.map_id {X : Type u_1} [TopologicalSpace X] : map (ContinuousMap.id X) = CategoryTheory.Functor.id (FundamentalGroupoid X)

@[simp]

theorem FundamentalGroupoid.map_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) : map (g.comp f) = (map f).comp (map g)

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

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

def FundamentalGroupoid.termπ : Lean.ParserDescr

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

def FundamentalGroupoid.termπₓ : Lean.ParserDescr

The fundamental groupoid of a topological space.

def FundamentalGroupoid.termπₘ : Lean.ParserDescr

The functor between fundamental groupoids induced by a continuous map.

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

@[reducible, inline]

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

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

@[reducible, inline]

abbrev FundamentalGroupoid.fromTop {X : TopCat} (x : ↑X) : ↑(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, inline]

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

@[reducible, inline]

abbrev FundamentalGroupoid.fromPath {X : Type u_1} [TopologicalSpace 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.

theorem FundamentalGroupoid.fromPath_eq_iff_homotopic {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (f g : Path x₀ x₁) : fromPath (Path.Homotopic.Quotient.mk f) = fromPath (Path.Homotopic.Quotient.mk g) ↔ f.Homotopic g

Two paths are equal in the fundamental groupoid if and only if they are homotopic.

theorem FundamentalGroupoid.eqToHom_eq {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (h : x₀ = x₁) : CategoryTheory.eqToHom ⋯ = ⟦(Path.refl x₁).cast h ⋯⟧

theorem FundamentalGroupoid.conj_eqToHom {X : Type u_1} [TopologicalSpace X] {x y x' y' : X} {p : Path x y} (hx : x' = x) (hy : y' = y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (Path.Homotopic.Quotient.mk p) (CategoryTheory.eqToHom ⋯)) = Path.Homotopic.Quotient.mk (p.cast hx hy)

theorem FundamentalGroupoid.conj_eqToHom_assoc {X : Type u_1} [TopologicalSpace X] {x y x' y' : X} {p : Path x y} (hx : x' = x) (hy : y' = y) {Z : FundamentalGroupoid X} (h : { as := y' } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (Path.Homotopic.Quotient.mk p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) = CategoryTheory.CategoryStruct.comp (Path.Homotopic.Quotient.mk (p.cast hx hy)) h