Principal bundles

Let \(B \in T\) be an object and let \(\Gg\) be a groupoid object in \(T\).

1. Let \(p\colon P \to B\) be an object of \(T_{/B}\) equipped with a \(\Gg\)-action over \(B\). We say that \(p\) is a formally principal \(\Gg\)-bundle over \(B\) if this action is regular as a \((\Gg \times B)\)-action in the slice \(T_{/B}\), i.e. if the shear map

   \[\shear_{1}\colon \Gg_1 \times_{\Gg_0} P \iso P \times_B P\]

   is an isomorphism.

2. A formally principal \(\Gg\)-bundle \(p\colon P \to B\) is called a principal \(\Gg\)-bundle if \(p\) is an effective epimorphism.

3. We write

   \[\Bun_{\Gg}(B) \quad \subseteq \quad \Act_{\Gg\times B}(T_{/B})\]

   for the full subcategory of principal \(\Gg\)-bundles over \(B\).