Classifying animae via principal bundles

Proof. A principal bundle is a locally trivial fiber bundle and hence a Serre fibration by Theorem 2.3.13. Since \(\Pi _{\infty }\colon \Top \to \An \) preserves pullbacks along Serre fibrations by Proposition 2.3.19, there are isomorphisms \[ \Piinfty {P \times _B \dots \times _B P} \iso \Piinfty {P} \times _{\Piinfty {B}} \dots \times _{\Piinfty {B}} \Piinfty {P} \] for all \(n\), which assemble into an isomorphism of simplicial animae \(\Piinfty {\check {C}(\pi )} \iso \check {C}(\Piinfty {\pi })\). By Lemma 9.2.10, the simplicial anima \(\Piinfty {\check {C}(\pi )}\) is isomorphic to \([n] \mapsto \Piinfty {P \times G^n}\). By contractibility of \(P\), the projection maps \(\Piinfty {P \times G^n} \cong \Pi _{\infty }(P) \times \Piinfty {G^n} \to \Piinfty {G^n}\) are isomorphisms, which are compatible with the simplicial structure maps (see Chapterexercise 5.1). This proves part (1). For part (2), observe that \(\Pi _{\infty }(\pi )\) is surjective on path components, since \(\pi \) is surjective. It is therefore an effective epimorphism of animae, so \(\Pi _{\infty }(B)\) is the colimit of its Čech nerve. On the other hand, the colimit of the simplicial anima underlying the group object \(\Pi _{\infty }(G)\) is its classifying anima \(\bB G\). Part (1) therefore gives the claimed isomorphism. □