Showing that $\lvert H K\rvert = \frac{| H\| K|}{ |H\cap K|}$ [duplicate]

I have seen a proof that for two subgroups $H$ and $K$ of a finite group $G$, $$|H K| = \frac{| H\| K\rvert}{| H\cap K|}$$ The proof counts the number of elements $hk$ that are the same as $h'k'$ for $h,h'\in H$ and $k,k'\in K$. I got confused with this proof.

My question is if there is another way to make things like this more clear. For example, I know that if one has a surjective homomorphism $f:G \to H$ then $\lvert G\rvert / \lvert \ker f\rvert = \lvert H\rvert$. That is, one can count the number of elements in something by essentially finding the order of the kernel of a map. This looks like what is going on with the product $HK$. But I guess that $HK$ in general isn't a group, so one can't talk about a group homomorphism.

Is there a way to find the "kernel" of a general function and get something like the first isomorphism theorem? All I would be interested in is how this can be used to count things.

$H\times K$ acts on $G$ (on the right) via $g\cdot(h,k)=h^{-1}gk$. Then $HK$ is the orbit of the identity element $e$, and so its size is $|H\times K|/|S_e|$ where $S_e$ is the stabiliser of $e$. Then $S_e=\{(h,h):k\in H\cap K\}$.

This method can also count the general double coset $HxK$.

Lemma: $\color{blue}{ H\times K/\mathcal R}$ has $n$ elements that is, $\color{blue}{n= |H\times K/\mathcal R| }$ and we have, $$\color{blue}{|HK|= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}}$$ This is a consequence of $E_1$ and $E_2$ see below for all the details.

Consider the map \begin{split} \phi :&& H\times K\to HK\\ && (h,k)\mapsto hk \end{split} Clearly, $\phi$ is onto (surjective ). Now we consider the relation,

$$\color{red}{(h,k)\mathcal R(h',k')\Longleftrightarrow hk=h'k'\Longleftrightarrow \phi(h,k)=\phi(h',k')}$$ It is easy to check that $\mathcal R$ is an equivalent relation on $H\times K$.

Fact.I. Let denote by $[h,k]_\mathcal R$ the class of an element $(h,k) \in H\times K.$

Let $n\in \mathbb N$ be the number of classes of $H\times K$ with respect to $\mathcal R.$ Also we denote by $\color{blue}{ H\times K/\mathcal R}$ the set of class. Precisely we have, $$\color{blue}{ H\times K/\mathcal R= \{[h_1,k_1]_\mathcal R, [h_2,k_2]_\mathcal R\cdots, [h_n,k_n]_\mathcal R\}}$$ Where, $(h_j,k_j)_j$ is a set of representative class of $H\times K/\mathcal R$.

First Equality: We consider the $\overline{\phi}$ the quotient map of $\phi$ w.r.t $\mathcal R.$ defines as follows:

\begin{split} \overline{\phi} :&& H\times K/\mathcal R \to HK\\ && [h,k]_\mathcal R \mapsto \phi(h,k) = hk \end{split}

• $\overline{\phi}$ is well define since from the red line above we have,

$$\color{red}{(h',k') \in [h,k]_\mathcal R\Longleftrightarrow (h,k)\mathcal R(h',k')\\\Longleftrightarrow hk=h'k'\Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}\tag{Eq}.$$ - It is also easy to check that $\overline{\phi}$ is one-to-one(injective) and Hence bijective since $\phi$ is onto. $$\color{red}{[h',k']_\mathcal R = [h,k]_\mathcal R\Longleftrightarrow (h',k') \in [h,k]_\mathcal R \Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}$$

conclusion $\overline{\phi}$ is a bijection and therfore, $$\color{blue}{n=|H\times K/\mathcal R| = |HK|}\tag{E_1}$$

we are jumping to the second equality, starting from the following observation.

Fact. II Since $\mathcal R$ is an equivalent relation, we know that $\color{red}{([h_j,k_j]_\mathcal R)_{1\le j\le n}}$ is a partition of $H\times K$ that is, $$\color{red}{ |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R| }$$ Claim:(see the proof Below) $$\color{red}{|[h_j,k_j]_\mathcal R| = |H\cap K|}$$

Second Equality: Since for any finte sets A and B we have $|A\times B| =|A|\times|B|,$ using the claim and the foregoing relations, we get that $$\color{blue}{|H|\times|K| = |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R| = \sum_{j=1}^{n} |H\cap K| =|H\times K/\mathcal R||H\cap K|}$$

Then $$\color{blue}{n= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}}\tag{E_2}$$

Proof of the claim: Now we would like to investigate $|[h,k]_\mathcal R|$.

$$\color{blue}{(h',k')\in [h,k]_\mathcal R \Longleftrightarrow hk=h'k'\Longleftrightarrow h'^{-1}h=k'k^{-1}\in H\cap K .}$$

Consider the map \begin{split} f :&& [h,k]_\mathcal R \to H\cap K\\ && (h',k')\mapsto h'^{-1}h=k'k^{-1} \end{split} The above relation shows that $f$ is well defined as a map. We will show that $f$ is a bijective map to conclude.

• $f$ is onto(surjective): Let $s\in H\cap K$. If we let $k' = h s^{-1}~~~\text{and}~~~ k'=sk$ then $\color{red}{h'k' = hs^{-1} sk =hk\Longleftrightarrow (h',k')\mathcal R (h,k) \implies (h',k') \in [h,k]_\mathcal R}$ and hence $$\color{red}{f(h',k')= f(hs^{-1}, sk)} = s.$$

this prove that $f$ is onto.

• $f$ is one-to-one(injective): let, $(a,b), (x,y)\in [h,k]_\mathcal R$ such that $f(a,b)=f(x,y)$. We have $f(a,b) =a^{-1}h =bk^{-1} ~~~~\text{and}~~~f(x,y) =x^{-1}h =yk^{-1}$

then, \begin{split} f(a,b)=f(x,y)&\implies& \color{blue}{a^{-1}h =bk^{-1}} =\color{red}{x^{-1}h =yk^{-1}}\\ &\implies& \color{blue}{a^{-1}h =x^{-1}h} ~~~~\text{and}~~~~\color{red}{ bk^{-1}=yk^{-1}}\\ &\implies& \color{red}{a =x} ~~~~\text{and}~~~~\color{red}{ b=y}\\ \end{split}

This proves that $f$ is bijective,s then the claim follows