Reading about Quantum Algorithms for finite-abelian groups one often encounters [1] the concept of orthogonal subgroups, a structure with a relatively simple definition.

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

It is not hard to see that $H^{\perp}$ is indeed subgroup of $G$. Orthogonal subgroups are somewhat similar to orthogonal complements, 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)

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

Question.

It intrigues me is that, 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.