Consider $H$ as a subgroup of $G$, we can push them to the level of classifying spaces $p: BH \rightarrow BG$. This is a covering space with fiber $[G:H]$.
What is the pullback of this covering map along the same map $p$?
Something that I know so far: the pullback bundle must also be a covering space with base space $BH$ and index equal to $[G:H]$. By the double coset formula, we can write the index $$[G:H] = \sum_{HxH \in H \G/H}[H: H \cap x^{-1}Hx].$$ Hence, my guess for the total space of the pullback is $$\coprod_{HxH \in H \G/H} B (H \cap x^{-1}Hx)$$,i.e., the disjoint union of the classifying space of $H \cap x^{-1}Hx$ over ${HxH \in H \G/H}$.
Could anyone provide some help? (Is my description of the total space correct? How do I prove it?)
It shall be awesome if you could upvote this question for me. Thank you!
Let $G$ be a finite group and $H, K \leq G$ subgroups. The canonical inclusion maps give rise to maps $BH \to BG$ and $BK \to BG$ of classifying spaces. We want to show that the pullback $$BH \times_{BG} BK \cong \coprod_{x \in H \backslash G / K} B(H \cap K^x).$$
The main step is the following set-theoretic calculation. Let $$\require{AMScd} \begin{CD} G/H \times G/K @>>> G/H \\ @VVV @VVV\\ G/K @>>> G/G \end{CD}$$ be a pullback of $G$-sets. Note that $G/H \times G/K$ is not necessarily a transitive $G$-set, but it can be decomposed into a union of such. The decomposition of $G/H \times G/K$ into $G$-orbits is given by the double coset formula: $$G/H \times G/K \cong \coprod_{x \in H \backslash G/K} G / (H \cap K^x).$$
If you haven't seen this before, you should try to prove it yourself. To start, note that every element in $G/H \times G/K$ is in the $G$-orbit of $(eH, xK)$ for some $x \in G$. Furthermore, $(eH, xK)$ and $(eH, x'K)$ belong to the same $G$-orbit iff $x$ and $x'$ belong to the same double coset of $H \backslash G / K$, so that the $G$-orbits of $G/H \times G/K$ are indexed by these double cosets. Finally, the stabilizer of $(eH, xK)$ is $H \cap K^x$. Putting this altogether yields the decomposition stated above.
There is an amusing remark in tom Dieck's book about how one can never remember Mackey's double coset formula, and contemplating this pullback square is how one should think about it.
Anyway, now apply homotopy orbits $(-)_{hG}$ to the pullback square above. Since homotopy orbits commute with homotopy pullbacks, we get another pullback square $$\begin{CD} \left(\coprod_{x \in H \backslash G/K} G / (H \cap K^x)\right)_{hG} @>>> (G/H)_{hG} \\ @VVV @VVV\\ (G/K)_{hG} @>>> (G/G)_{hG}. \end{CD}$$
Simplifying, we see that the square $$\begin{CD} \coprod_{x \in H \backslash G/K} B(H \cap K^x) @>>> BH \\ @VVV @VVV\\ BK @>>> BG \end{CD}$$ is a pullback, as desired.