Homotopy fiber of a map between classifying spaces

I'm looking for a reference (and precise hypothesis if more are needed) for the following facts (or a correction, if I'm just plain wrong):

Let $G$ and $H$ be topological groups and $f : G \to H$ be a continuous homomorphism. Applying the classifying space functor gives a map $Bf: BG \to BH$.

1. The homotopy fiber of $Bf$ is the homotopy orbit space $H_{hG}$ where $G$ acts on $H$ via $g \cdot h = f(g)h$.

2. The canonical map $H_{hG} \to H/G = H/\mathrm{im} f$ has homotopy fiber given by $BK$ where $K = \ker f$.

Maybe more well-known that those are the corollaries for when $f$ is either injective or surjective:

1. If $G$ is a subgroup of $H$, the homotopy fiber of the map induced by the inclusion $BG \to BH$ is the coset space $H/G$.

2. If $1 \to K \to G \to H \to 1$ is a short exact sequence of topological groups, applying the classifying space functor gives a fiber sequence $BK \to BG \to BH$.

EDIT: I sketched a proof here. I'm mostly looking for references, but would also appreciate alternate proofs (specially a proof that avoids using the generalized Mather cube property on a diagram whose shape is not a 1-category).

EDIT 2: Tyler Lawson's nice example shows that more hypothesis are needed for part 2 of the "fact" and for corollary 1. My current guess is that for corollary 1, it is enough that $H \to H/G$ locally have a section.

• I'm interested in the answers as well but I imagine they all go back to at least Borel, perhaps earlier. – Ryan Budney Apr 6 '16 at 20:38
• Borel sounds pretty likely, @RyanBudney. – Omar Antolín-Camarena Apr 6 '16 at 20:53
• I don't have a reference, but doesn't an answer to the first question follow from the fact that the homotopy fiber of $Bf$ is the classifying space of a category whose objects are elements of $H$ and morphisms $h \to h'$ consist of $g \in G$ so that $f(g)h' = h$? – Vidit Nanda Apr 6 '16 at 20:58
• @ViditNanda: Well, (1) it does follow from that, but you'd need to prove that :); (2) I think your characterization is easy to prove if G and H are discrete, is it also easy in general? – Omar Antolín-Camarena Apr 6 '16 at 21:08
• @OmarAntolín-Camarena So just to confirm, what is your preferred definition of the homotopy fiber of $Bf$? – Vidit Nanda Apr 6 '16 at 21:39

Your sketch doesn't say very much about the topologies involved, and I did wonder if, for example, you need $im f$ closed for your coset space identification.
• I think the only spot I might need some sort of hypothesis on the topology in that sketch is the two places where I use that if the action of $G$ on some $X$ is free, then $X_{hG}$ is (weakly) homotopy equivalent to $X/G$. I just realized I don't know exactly what's needed for that to hold. Maybe that needs that $X \to X/G$ is a principal $G$-bundle. – Omar Antolín-Camarena Apr 7 '16 at 1:44