The fundamental groupoid of a simply connected space

A space is simply connected exactly when its fundamental groupoid is codiscrete: there is one and only one morphism between any two of its objects. This file records that uniqueness as a Unique instance on the hom types, so that a transport map along a path inside a simply connected space can be written down without naming the path, and two such transports agree because the morphisms realizing them are equal.

The two lemmas about a functor out of such a groupoid say that the resulting transport maps compose as expected and that the unique endomorphism of an object is sent to an identity.

@[instance_reducible]

noncomputable instance FundamentalGroupoid.instUniqueHom {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] (x y : FundamentalGroupoid X) : Unique (x ⟶ y)

In a simply connected space there is exactly one morphism of the fundamental groupoid between any two points; default is that morphism.

Equations

• x.instUniqueHom y = ⋯.some

@[simp]

theorem CategoryTheory.Functor.map_default_self {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {D : Type u_2} [Category.{u_3, u_2} D] (F : Functor (FundamentalGroupoid X) D) (x : FundamentalGroupoid X) : F.map default = CategoryStruct.id (F.obj x)

A functor out of the fundamental groupoid of a simply connected space sends the unique endomorphism of an object to the identity.

@[simp]

theorem CategoryTheory.Functor.map_default_comp {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {D : Type u_2} [Category.{u_3, u_2} D] (F : Functor (FundamentalGroupoid X) D) (x y z : FundamentalGroupoid X) : CategoryStruct.comp (F.map default) (F.map default) = F.map default

A functor out of the fundamental groupoid of a simply connected space sends the unique morphisms x ⟶ y and y ⟶ z to maps whose composite is the image of the unique morphism x ⟶ z.

@[simp]

theorem CategoryTheory.Functor.map_default_comp_assoc {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {D : Type u_2} [Category.{u_3, u_2} D] (F : Functor (FundamentalGroupoid X) D) (x y z : FundamentalGroupoid X) {Z : D} (h : F.obj z ⟶ Z) : CategoryStruct.comp (F.map default) (CategoryStruct.comp (F.map default) h) = CategoryStruct.comp (F.map default) h

A functor out of the fundamental groupoid of a simply connected space sends the unique morphisms x ⟶ y and y ⟶ z to maps whose composite is the image of the unique morphism x ⟶ z.