Represent a transformation by
Multiplication preserves this form and determinant, and the inverse has the same form with parameters . To check the congruence condition, complex conjugation is the identity modulo . Thus says exactly that fixes the column modulo two. Products and inverses preserve this property. The identity belongs to the set, and changing the common sign of does not change either the transformation or its congruence. Hence these transformations form a group.
Because , the denominator has no zero in the disc. Direct calculation gives
The inverse also maps the disc into itself, so is a disc automorphism, and these identities show that it preserves the hyperbolic metric .
The action is properly discontinuous. If is compact, put . If , choose with . Then
Since and , its distance bound gives and therefore . There are only finitely many Gaussian integers with these bounds, so only finitely many satisfy . This proves the required properly discontinuous group action directly.
If , then and is one of the Gaussian units . The congruence leaves only . Both give the identity transformation. Thus the point stabilizer of zero is trivial.
The closed Dirichlet region centered at zero is the set of with for every . For a nonidentity element, . Write
The distance inequality is equivalent, by pseudohyperbolic distance, to . Squaring and subtracting yields
Since and , the bisector half-plane is exactly
For or and or , all the group conditions hold and the products are the four numbers , with . Their four inequalities force
Conversely, for any group element . As are integers, . Thus every point satisfying those four inequalities satisfies every other one:
This proves, with no missing bisectors, the Gaussian-integer disc group with an ideal-square Dirichlet domain formula
Equivalently it is the part of the unit disc outside all four open circles of radius one centered at . Its sides are the inward arcs of those circles. They meet the unit circle orthogonally, and their ideal vertices are ; these vertices themselves lie outside the open disc.
Figure 1.
Origin-centered Dirichlet region and the four neighboring orbit points
. Details.
The origin has trivial point stabilizer and the group orbit is locally finite by the discontinuity proof, so this closed bisector intersection has translates covering the disc with disjoint interiors, as in the definition of a Dirichlet domain. Side identifications are allowed on its boundary.