Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

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

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} (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

Auxiliary function for trans_refl_reparam.

Equations
theorem Path.Homotopy.trans_refl_reparam {X : Type u} [TopologicalSpace 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} (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} (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

Auxiliary function for trans_assoc_reparam.

Equations
theorem Path.Homotopy.trans_assoc_reparam {X : Type u} [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) => Path.Homotopy.transAssocReparamAux t, )
def Path.Homotopy.transAssoc {X : Type u} [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).

Equations
  • One or more equations did not get rendered due to their size.
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.

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

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
@[simp]
theorem FundamentalGroupoid.equiv_symm_apply_as (X : Type u_1) (x : X) :
((FundamentalGroupoid.equiv X).symm x).as = x
Equations
  • FundamentalGroupoid.instInhabited = { default := { as := default } }
Equations

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

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

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

Equations

The fundamental groupoid of a topological space.

Equations

The functor between fundamental groupoids induced by a continuous map.

Equations
theorem FundamentalGroupoid.map_eq {X Y : TopCat} {x₀ x₁ : X} (f : C(X, Y)) (p : Path.Homotopic.Quotient x₀ x₁) :
@[reducible, inline]

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

Equations
@[reducible, inline]

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

Equations
@[reducible, inline]
abbrev FundamentalGroupoid.toPath {X : TopCat} {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
@[reducible, inline]
abbrev FundamentalGroupoid.fromPath {X : TopCat} {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