Reading about Quantum Algorithms for finite-abelian groups one often encounters [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, 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)

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.