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
.
Instances For
For any path p
from x₀
to x₁
, we have a homotopy from the constant path based at x₀
to
p.trans p.symm
.
Instances For
For any path p
from x₀
to x₁
, we have a homotopy from the constant path based at x₁
to
p.symm.trans p
.
Instances For
Auxiliary function for trans_refl_reparam
.
Instances For
For any path p
from x₀
to x₁
, we have a homotopy from p.trans (Path.refl x₁)
to p
.
Instances For
For any path p
from x₀
to x₁
, we have a homotopy from (Path.refl x₀).trans p
to p
.
Instances For
Auxiliary function for trans_assoc_reparam
.
Instances For
For paths p q r
, we have a homotopy from (p.trans q).trans r
to p.trans (q.trans r)
.
Instances For
The fundamental groupoid of a space X
is defined to be a type synonym for X
, and we
subsequently put a CategoryTheory.Groupoid
structure on it.
Instances For
The functor sending a topological space X
to its fundamental groupoid.
Instances For
Help the typechecker by converting a point in a groupoid back to a point in the underlying topological space.
Instances For
Help the typechecker by converting a point in a topological space to a point in the fundamental groupoid of that space.
Instances For
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
).
Instances For
Help the typechecker by converting a path in a topological space to an arrow in the fundamental groupoid of that space.