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.

source
noncomputable def path.homotopy.refl_trans_symm_aux (x : ↥unit_interval × ↥unit_interval) :
ℝ

Auxilliary function for refl_trans_symm

Equations
source
@[continuity]
theorem path.homotopy.continuous_refl_trans_symm_aux  :
continuous path.homotopy.refl_trans_symm_aux
source
theorem path.homotopy.refl_trans_symm_aux_mem_I (x : ↥unit_interval × ↥unit_interval) :
path.homotopy.refl_trans_symm_aux x ∈ unit_interval
source
noncomputable def path.homotopy.refl_trans_symm {X : Type u} [topological_space 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
source
noncomputable def path.homotopy.refl_symm_trans {X : Type u} [topological_space 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
source
noncomputable def path.homotopy.trans_refl_reparam_aux (t : ↥unit_interval) :
ℝ

Auxilliary function for trans_refl_reparam

Equations
source
@[continuity]
theorem path.homotopy.continuous_trans_refl_reparam_aux  :
continuous path.homotopy.trans_refl_reparam_aux
source
theorem path.homotopy.trans_refl_reparam_aux_mem_I (t : ↥unit_interval) :
path.homotopy.trans_refl_reparam_aux t ∈ unit_interval
source
theorem path.homotopy.trans_refl_reparam_aux_zero  :
path.homotopy.trans_refl_reparam_aux 0 = 0
source
theorem path.homotopy.trans_refl_reparam_aux_one  :
path.homotopy.trans_refl_reparam_aux 1 = 1
source
theorem path.homotopy.trans_refl_reparam {X : Type u} [topological_space X] {x₀ x₁ : X} (p : path x₀ x₁) :
p.trans (path.refl x₁) = p.reparam (λ (t : ↥unit_interval), ⟨path.homotopy.trans_refl_reparam_aux t, _⟩) _ _ _
source
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
source
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
source
noncomputable def path.homotopy.trans_assoc_reparam_aux (t : ↥unit_interval) :
ℝ

Auxilliary function for trans_assoc_reparam.

Equations
source
@[continuity]
theorem path.homotopy.continuous_trans_assoc_reparam_aux  :
continuous path.homotopy.trans_assoc_reparam_aux
source
theorem path.homotopy.trans_assoc_reparam_aux_mem_I (t : ↥unit_interval) :
path.homotopy.trans_assoc_reparam_aux t ∈ unit_interval
source
theorem path.homotopy.trans_assoc_reparam_aux_zero  :
path.homotopy.trans_assoc_reparam_aux 0 = 0
source
theorem path.homotopy.trans_assoc_reparam_aux_one  :
path.homotopy.trans_assoc_reparam_aux 1 = 1
source
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₃) :
(p.trans q).trans r = (p.trans (q.trans r)).reparam (λ (t : ↥unit_interval), ⟨path.homotopy.trans_assoc_reparam_aux t, _⟩) _ _ _
source
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
source
def fundamental_groupoid (X : Type u) :
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
source
@[protected, instance]
def fundamental_groupoid.inhabited {X : Type u} [h : inhabited X] :
inhabited (fundamental_groupoid X)
Equations
source
@[protected, instance]
noncomputable def fundamental_groupoid.category_theory.groupoid {X : Type u} [topological_space X] :
category_theory.groupoid (fundamental_groupoid X)
Equations
source
theorem fundamental_groupoid.comp_eq {X : Type u} [topological_space X] (x y z : fundamental_groupoid X) (p : x ⟶ y) (q : y ⟶ z) :
p ≫ q = path.homotopic.quotient.comp p q
source
theorem fundamental_groupoid.id_eq_path_refl {X : Type u} [topological_space X] (x : fundamental_groupoid X) :
𝟙 x = ⟦path.refl x⟧
source
noncomputable def fundamental_groupoid.fundamental_groupoid_functor  :
Top ⥤ category_theory.Groupoid

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

Equations
source
theorem fundamental_groupoid.map_eq {X Y : Top} {x₀ x₁ : ↥X} (f : C(↥X, ↥Y)) (p : path.homotopic.quotient x₀ x₁) :
(fundamental_groupoid.fundamental_groupoid_functor.map f).map p = p.map_fn f
source
@[reducible]
def fundamental_groupoid.to_top {X : Top} (x : ↥(fundamental_groupoid.fundamental_groupoid_functor.obj X)) :
↥X

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

Equations
source
@[reducible]
def fundamental_groupoid.from_top {X : Top} (x : ↥X) :
↥(fundamental_groupoid.fundamental_groupoid_functor.obj X)

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

Equations
source
@[reducible]
def fundamental_groupoid.to_path {X : Top} {x₀ x₁ : ↥(fundamental_groupoid.fundamental_groupoid_functor.obj X)} (p : x₀ ⟶ x₁) :
path.homotopic.quotient x₀ x₁

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
source
@[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