Basic results on fundamental groupoids

This file records basic facts about fundamental groupoids used when comparing the fundamental groupoid of a space with those of its subspaces: the functor induced by an injective continuous map is injective on objects (as CategoryTheory.Subgroupoid.im requires), membership of a path class in a subgroupoid is unchanged by transporting its endpoints along equalities, and the induced functor of a composite acts on a single morphism as the composite of the induced functors.

Main declarations

• ContinuousMap.fundamentalGroupoid_map_obj_injective: an injective continuous map induces a functor of fundamental groupoids that is injective on objects.
• Path.Homotopic.Quotient.cast_mem_arrows_iff: membership of a path class in a subgroupoid of the fundamental groupoid is unchanged by casting its endpoints along equalities.
• FundamentalGroupoid.map_comp_map: the morphism-level form of FundamentalGroupoid.map_comp.

@[simp]

theorem Path.Homotopic.Quotient.cast_mem_arrows_iff {X : Type u_1} [TopologicalSpace X] {S : CategoryTheory.Subgroupoid (FundamentalGroupoid X)} {a b a' b' : X} (q : Homotopic.Quotient a b) (ha : a' = a) (hb : b' = b) : q.cast ha hb ∈ S.arrows { as := a' } { as := b' } ↔ q ∈ S.arrows { as := a } { as := b }

Membership of a path class in a subgroupoid of the fundamental groupoid is unchanged by casting its endpoints along equalities.

theorem FundamentalGroupoid.map_comp_map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) {a b : FundamentalGroupoid X} (p : a ⟶ b) : (map (g.comp f)).map p = (map g).map ((map f).map p)

The morphism-level form of FundamentalGroupoid.map_comp. The source and target of the two sides agree definitionally, so unlike the equality of functors this form needs no eqToHom.

theorem ContinuousMap.fundamentalGroupoid_map_obj_injective {X : Type u_1} {A : Type u_2} [TopologicalSpace X] [TopologicalSpace A] (f : C(X, A)) (hf : Function.Injective ⇑f) : Function.Injective (FundamentalGroupoid.map f).obj

The functor between fundamental groupoids induced by an injective continuous map is injective on objects.