The fundamental groupoid on a set of basepoints

For a set S of points of a topological space X, the fundamental groupoid of X on S is the full subgroupoid of the fundamental groupoid of X whose objects are the points of S: its morphisms from s to t are the homotopy classes of paths in X from s to t. Choosing S to meet every path component of the spaces involved keeps the groupoid small while losing no information, which is what makes the groupoid Seifert--van Kampen theorem a practical tool for calculations, for instance on the circle covered by two arcs, where two basepoints are needed.

Main declarations

• TauCeti.FundamentalGroupoidOn: the fundamental groupoid of X on a set of basepoints.
• TauCeti.FundamentalGroupoidOn.incl: its inclusion into the fundamental groupoid of X.
• TauCeti.FundamentalGroupoidOn.map: the functor induced by a continuous map sending one set of basepoints into another, with map_id and map_comp.
• TauCeti.FundamentalGroupoidOn.instSubsingletonHom: on a simply connected space, there is at most one morphism between two basepoints.

References

• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7.

@[reducible, inline]

abbrev TauCeti.FundamentalGroupoidOn {X : Type u_1} (S : Set X) : Type u_1

The fundamental groupoid of X on a set S of basepoints: the full subgroupoid of the fundamental groupoid of X whose objects are the points of S.

Equations

• TauCeti.FundamentalGroupoidOn S = CategoryTheory.InducedCategory (FundamentalGroupoid X) fun (s : ↑S) => { as := ↑s }

@[reducible, inline]

noncomputable abbrev TauCeti.FundamentalGroupoidOn.incl {X : Type u_1} [TopologicalSpace X] (S : Set X) : CategoryTheory.Functor (FundamentalGroupoidOn S) (FundamentalGroupoid X)

The inclusion of the fundamental groupoid on S into the fundamental groupoid of X.

Equations

• TauCeti.FundamentalGroupoidOn.incl S = CategoryTheory.inducedFunctor fun (s : ↑S) => { as := ↑s }

noncomputable def TauCeti.FundamentalGroupoidOn.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {T : Set Y} (f : C(X, Y)) (hf : Set.MapsTo (⇑f) S T) : CategoryTheory.Functor (FundamentalGroupoidOn S) (FundamentalGroupoidOn T)

The functor between fundamental groupoids on sets of basepoints induced by a continuous map f sending S into T.

Equations

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

@[simp]

theorem TauCeti.FundamentalGroupoidOn.map_obj {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {T : Set Y} (f : C(X, Y)) (hf : Set.MapsTo (⇑f) S T) (s : FundamentalGroupoidOn S) : (map f hf).obj s = ⟨f ↑s, ⋯⟩

@[simp]

theorem TauCeti.FundamentalGroupoidOn.map_map_hom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {T : Set Y} (f : C(X, Y)) (hf : Set.MapsTo (⇑f) S T) {s t : FundamentalGroupoidOn S} (g : s ⟶ t) : ((map f hf).map g).hom = (FundamentalGroupoid.map f).map g.hom

@[simp]

theorem TauCeti.FundamentalGroupoidOn.map_comp_incl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {T : Set Y} (f : C(X, Y)) (hf : Set.MapsTo (⇑f) S T) : (map f hf).comp (incl T) = (incl S).comp (FundamentalGroupoid.map f)

The functor induced by f is compatible with the inclusions.

@[simp]

theorem TauCeti.FundamentalGroupoidOn.map_id {X : Type u_1} [TopologicalSpace X] {S : Set X} : map (ContinuousMap.id X) ⋯ = CategoryTheory.Functor.id (FundamentalGroupoidOn S)

The identity map induces the identity functor.

theorem TauCeti.FundamentalGroupoidOn.map_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {T : Set Y} {U : Set Z} (g : C(Y, Z)) (f : C(X, Y)) (hg : Set.MapsTo (⇑g) T U) (hf : Set.MapsTo (⇑f) S T) : map (g.comp f) ⋯ = (map f hf).comp (map g hg)

The functor induced by a composite is the composite of the induced functors.

instance TauCeti.FundamentalGroupoidOn.instSubsingletonHom {X : Type u_1} [TopologicalSpace X] {S : Set X} [SimplyConnectedSpace X] (s t : FundamentalGroupoidOn S) : Subsingleton (s ⟶ t)

In the fundamental groupoid of a simply connected space on a set of basepoints, there is at most one morphism between two objects.