This entry is about ( a fragment of) a paper by Anders Kock
Pregroupoids derived from a groupoid
Let a groupoid, subsets.
Then the object defined to be the set of arrows in whose source is in and whose target is in equipped with the two evident structure maps
is a pregroupoid. If this is a full subgroupoid of .
Pregroupoid associated to a principal bundle
Let be a principal right -bundle for a group . Then the span is a pregroupoid.
The category of pregroupoids
There is a category with pregroupoids as objects and triples of morphisms making
There is a forgetful functor
Groupoids associated to a pregroupoid
There are three candidates of a groupoid associated to a pregroupoid: , and . and are called edges of the pregroupoid , since they appear as edges of some bisimplicial set. is called enveloping groupoid for the pregroupoid . contains the edges of as subgroupoids.
The Ehresmann groupoid
For a pregroupoid the Ehresmann groupoid is defined by and
The ”inverse Ehresmann” groupoid
For a pregroupoid the ”inverse Ehresmann” groupoid is defined by and
If is a principal -bundle, the groupoid is canonically isomorphic to the one object groupoid by
The enveloping groupoid
Let be a pregroupoid.
The enveloping groupoid for is defined by and , where denotes the pregroupoid with and interchanged. And calculations (see arxiv p.9) show that this is a groupoid.
The edges of act on principally on the left and the right, respectively and the actions commute with each other.
Let be a principal bundle. Then there is a groupoid with and . In this cases
The functor is a faithful left adjoint to the forgetful functor , the unit for the adjunction is injective.
- Principal bundles, groupoids and connections (arxiv),