mathlib3 documentation

algebraic_topology.fundamental_groupoid.basic

Fundamental groupoid of a space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Auxilliary function for refl_trans_symm

Equations
noncomputable def path.homotopy.refl_trans_symm {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :

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
noncomputable def path.homotopy.refl_symm_trans {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :

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

Auxilliary function for trans_refl_reparam

Equations
theorem path.homotopy.trans_refl_reparam {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :
noncomputable def path.homotopy.trans_refl {X : Type u} [topological_space 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
noncomputable def path.homotopy.refl_trans {X : Type u} [topological_space 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

Auxilliary function for trans_assoc_reparam.

Equations
theorem path.homotopy.trans_assoc_reparam {X : Type u} [topological_space X] {x₀ x₁ x₂ x₃ : X} (p : path x₀ x₁) (q : path x₁ x₂) (r : path x₂ x₃) :
noncomputable def path.homotopy.trans_assoc {X : Type u} [topological_space 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
def fundamental_groupoid (X : Type u) :

The fundamental groupoid of a space X is defined to be a type synonym for X, and we subsequently put a category_theory.groupoid structure on it.

Equations
Instances for fundamental_groupoid

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

Equations
@[reducible]

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

Equations
@[reducible]

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

Equations
@[reducible]

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]
def fundamental_groupoid.from_path {X : Top} {x₀ x₁ : X} (p : path.homotopic.quotient x₀ x₁) :
x₀ x₁

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

Equations