Fiber product of groups (source code)

= Fiber product of groups

For <homomorphisms> $E\to H$ and $G\to H$, their fiber product is
$$
E\times_HG=\{(e,g)\in E\times G:\pi(e)=f(g)\}.
$$
It is a <subgroup> of $E\times G$. Pulling a <group extension> back along $G\to H$ uses this fiber product as its middle group.