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$$

> Where $\chi_g$ are the characters of $G$.

This structure resembles [orthogonal complements][2], for using standard group-theory one obtains the following properties

> Given two subgroups $H$ and $K$ of $G$:

> 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, some collaborators and I can only find proofs of propositions (1-3) in *relatively-recent research papers*. Moreover, we have never seen 4. proven anywhere. I would like to find out whether if this concept  is well-known in pure mathematics or its somewhat new, **and**, if there are **books** where propositions (1-4) are proven to cite in papers. Ideally, the proofs should be for *finite* abelian groups.

**Note:**  I can proof  (1-4) using standard group-theory. If there is a smarter more-general way of proving them I would also be  interested.

  [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