A canonical construction proving $\left|HK\right| = \left|H\right|\left|K\right| / \left|H \cap K\right|$? Let $H$ and $K$ be subgroups of a finite group $G$.  A standard
result is the formula $$\left|HK\right| =
\frac{\left|H\right|\left|K\right|}{\left|H \cap K\right|}$$ for
the cardinality of the set $HK$.
The proofs of this that I've seen always involve some arbitrary
choice, such as the choice of a transversal for $\{hK \colon 
h \in H\}$.
Is there a way to show that these quantities are equal without
making such an arbitrary choice?  For example, can they be shown
to be the respective dimensions of a pair of canonically
isomorphic modules?
 A: You can also prove the assertion in the setting of group actions. Note that the group $H \times K$ acts transitively on the set $HK$ by $(h, k) * x := hxk^{-1}$ for each $x \in HK$. The stabilizer of the element $1 \in HK$ is obviously isomorphic to $H \cap K$. So the assertion follows by the orbit stabilizer theorem.
A: Define $\pi:H\times K\to HK$ by $(h,k)\to hk$.
Note that for all $hk\in HK$, the map $\sigma$: $\pi^{-1}(hk)\to H\cap K$ by $(h',k')\mapsto h'h^{-1}=k'k^{-1}\in H\cap K$ is bijective.
Thus $\forall hk \in HK, |\{(h',k')\in H\times K:hk=h'k'\}|=|\pi^{-1}(hk)|=|H\cap K|$. Therefore, $|HK||H\cap K|=|H\times K|=|H||K|$.
Edited:
As Artuo commented below, we have to take care of the representative of each $hk$ in HK. I fixed the problem in the following version, But the idea remains the same. You can read the previous version, which is perhaps more intuitive, with the representative of $hk$ in mind.
Define $\pi:H\times K\to HK$ by $(h,k)\to hk$.
Note that for all $x\in HK$, $x=hk$ for some $h\in H, k\in K$. The map $\sigma$: $\pi^{-1}(x)\mapsto H\cap K$ by $(h',k')\to h'h^{-1}=k'k^{-1}\in H\cap K$ is bijective.
Thus $\forall x \in HK, |\pi^{-1}(x)|=|H\cap K|$.
If we take $x=(h,k)$, then $|\{(h',k')\in H\times K:hk=h'k'\}|=|\pi^{-1}(x)|=|H\cap K|$.
Therefore, $|HK||H\cap K|=|H\times K|=|H||K|$.
A: Sure. In fact, we can prove “it” in general, without assuming $G$ is finite (quotation marks because we will actually prove a different equality, from which this one can be deduced in the finite case).
We define a map from $H\times K$ to $HK$. The maps sends $(h,k)$ to $hk$.
Then we figure out the size of each fiber:
First, let $d\in H\cap K$. Then the pair $(hd,d^{-1}k)$ maps to the element $(h,k)$. Thus, there are at least $|H\cap K|$ elements in each fiber.
Now suppose that $(h,k)$ and $(h’,k’)$ map to the same thing. That is, that $hk=h’k’$. Then $(h’)^{-1}h=k’k^{-1}=d\in H\cap K$. That is, $h=h’d$ and $k=d^{-1}k’$, so that the pair $(h,k)$ is equal to the pair $(h’d,d^{-1}k’)$. So every element in the fiber of $(h,k)$ is of the form above.
Thus, the cardinality of the domain equals the cardinality of the image times the size of the fibers (since all fibers have the same size), so
$$|H||K| = |HK||H\cap K|.$$
In the case where all quantities are finite (for example, if $G$ is finite, or if $HK$ is finite), then we can divide through by $|H\cap K|$ to get
$$|HK| = \frac{|H||K|}{|H\cap K|},$$
the desired equality.
A: The equivalence relation $(h,k)\sim (h',k')\stackrel{(def.)}{\iff} hk=h'k'$ induces a partition of $H\times K$ into equivalence classes each of cardinality $|H\cap K|$, and the quotient set $(H\times K)/\sim$ has cardinality $|HK|$. Therefore, if $H$ and $K$ are finite (in particular if they are subgroups of a finite group), we get: $|H\times K|=|H||K|=|H\cap K| |HK|$, whence the formula in the OP. Hereafter the details.

Let's define in $H\times K$ the equivalence relation: $(h,k)\sim (h',k')\stackrel{(def.)}{\iff} hk=h'k'$. The equivalence class of $(h,k)$ is given by:
$$[(h,k)]_\sim=\{(h',k')\in H\times K\mid h'k'=hk\} \tag 1$$
Now define the following map from any equivalence class:
\begin{alignat*}{1}
  f_{(h,k)}:[(h,k)]_\sim &\longrightarrow&  H\cap K \\
  (h',k')&\longmapsto& f_{(h,k)}((h',k')):=k'k^{-1} \\
\tag 2
 \end{alignat*}
Note that $k'k^{-1}\in K$ by closure of $K$, and $k'k^{-1}\in H$ because $k'k^{-1}=h'^{-1}h$ (being $(h',k')\in [(h,k)]_\sim$) and by closure of $H$. Therefore, indeed $k'k^{-1}\in H\cap K$.
Lemma 1. $f_{(h,k)}$ is bijective.
Proof.
\begin{alignat}{2}
f_{(h,k)}((h',k'))=f_{(h,k)}((h'',k'')) &\space\space\space\Longrightarrow &&k'k^{-1}=k''k^{-1} \\
&\space\space\space\Longrightarrow &&k'=k'' \\
&\stackrel{h'k'=h''k''}{\Longrightarrow} &&h'=h'' \\
&\space\space\space\Longrightarrow &&(h',k')=(h'',k'') \\
\end{alignat}
and the map is injective. Then, for every $a\in H\cap K$, we  get $ak\in K$ and $a=f_{(h,k)}((h',ak))$, and the map is surjective. $\space\space\Box$
Now define the following map from the quotient set:
\begin{alignat}{1}
  f:(H\times K)/\sim &\longrightarrow&  HK \\
  [(h,k)]_\sim &\longmapsto& f([(h,k)]_\sim):=hk \\
\tag 3
 \end{alignat}
Lemma 2. $f$ is well-defined and bijective.
Proof.

*

*Good definition: $(h',k')\in [(h,k)]_\sim \Rightarrow f([(h',k')]_\sim)=h'k'=hk=f([(h,k)]_\sim)$;

*Injectivity: $f([(h',k')]_\sim)=f([(h,k)]_\sim) \Rightarrow h'k'=hk \Rightarrow (h',k')\in [(h,k)]_\sim \Rightarrow [(h',k')]_\sim=[(h,k)]_\sim$;

*Surjectivity: for every $ab\in HK$ , we get $ab=f([(a,b)]_\sim)$. $\space\space\Box$
