Reading about Quantum Algorithms for **finite-abelian** groups one often encounters [\[1\]][1] the concept of **orthogonal subgroups**

> Let $G$ be a finite abelian group, then the orthogonal subgroup $H^{\perp}$ of $H$ a subgroup of $G$ is defined as:

> $$H^\perp:=\lbrace g\in H : \chi_g(h)=1 \quad\text{for all } h \in H\rbrace$$

Orthogonal subgroups are somewhat similar to [orthogonal complements][2], for using standard group-theory one finds that the fulfil the following properties

For two subgroups $H$ and $K$:

 1. $H^{\perp^{\perp}} = H$
 2. $|H^{\perp}| = |G|/|H|$
 3. $H\subset K$ if and only if $K^{\perp}\subset H^{\perp}$ 
 4. $(H\cap K)^{\perp} = H^{\perp} ∨ K^{\perp}$ (where $∨$ denotes the [join][3])

Yet they are not orthogonal complements since $H\cap K = \lbrace 0 \rbrace$ does not hold in general.


**Question**.

In spite of the simplicity of the definition above, I have only found proofs of propositions (1-3) in *relatively-recent research papers*, and I can not find 4. proven anywhere. I would like to know if this concept  is well-known in pure mathematics **and**, if there are **books** where propositions (1-4) are proven that I could cite in papers. *Ideally*, the proofs should be for *finite* abelian groups.

**Note:** I do not need *new* proofs of these properties.

  [1]: http://arxiv.org/abs/quant-ph/0411037
  [2]: http://en.wikipedia.org/wiki/Orthogonal_complement
  [3]: http://groupprops.subwiki.org/wiki/Join_of_subgroups