By extensionality on \(\operatorname {GL}\) elements, it suffices to check all entries \((i,j)\) with \(i,j \in \{ 0,1\} \). Each entry is verified by simplification using the definition of \(\operatorname {unipotentGL}\).

By extensionality on \(\operatorname {GL}\) elements, it suffices to check all entries \((i,j)\) with \(i,j \in \{ 0,1\} \). Each entry equality is verified by simplification using the definition of \(\operatorname {unipotentGL}\), the matrix multiplication formula, and ring arithmetic.

Let \(a, b \in \mathbb {Z}/q\mathbb {Z}\) with \(\operatorname {unipotentPGL}(q,a) = \operatorname {unipotentPGL}(q,b)\). Unfolding the definition of \(\operatorname {projPGL}\) and using the quotient group equality, we obtain that

lies in the center of \(\operatorname {GL}(2, \mathbb {F}_q)\), i.e., \(k \cdot z = z \cdot k\) for all \(k\).

We compute \(z.\operatorname {val} = \begin{pmatrix} 1 & b-a \\ 0 & 1 \end{pmatrix}\) by multiplying \(\begin{pmatrix} 1 & -a \\ 0 & 1 \end{pmatrix}\begin{pmatrix} 1 & b \\ 0 & 1 \end{pmatrix}\) and simplifying.

Since \(z\) is in the center, it commutes with \(E_{21} = \operatorname {matToGL}\! \left(\begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}\right)\). From the \((0,0)\)-entry of the commutation identity \(E_{21} \cdot z.\operatorname {val} = z.\operatorname {val} \cdot E_{21}\), we extract by simplification that \(b - a = 0\), hence \(a = b\).

This follows directly by simplification using the definitions of \(\operatorname {unipotentSubgroup}\), \(\operatorname {MonoidHom.mem_range}\), and \(\operatorname {unipotentPGLHom_apply}\).

We first show \(\operatorname {unipotentPGLHom}(q)\) is injective. Let \(a, b\) with \(\operatorname {unipotentPGLHom}(q)(a) = \operatorname {unipotentPGLHom}(q)(b)\). Unfolding the definition of \(\operatorname {unipotentPGLHom}\), this gives \(\operatorname {unipotentPGL}(q, \operatorname {toAdd}(a)) = \operatorname {unipotentPGL}(q, \operatorname {toAdd}(b))\), and by \(\operatorname {unipotentPGL_injective}\) we get \(\operatorname {toAdd}(a) = \operatorname {toAdd}(b)\), hence \(a = b\).

Using injectivity, we construct a bijection

via \(x \mapsto (\operatorname {unipotentPGLHom}(q)(x), \langle x, \operatorname {rfl}\rangle )\). Rewriting with this cardinality equivalence, and using \(|\operatorname {Multiplicative}(\mathbb {Z}/q\mathbb {Z})| = |\mathbb {Z}/q\mathbb {Z}| = q\), we obtain \(|\operatorname {unipotentSubgroup}(q)| = q\).

Rewriting with \(\operatorname {unipotentSubgroup_card}\), the goal becomes showing \(q\) is odd. Rewriting with \(\operatorname {Nat.odd_iff}\), this is exactly the hypothesis \(q \% 2 = 1\).

By simplification using the \(2 \times 2\) determinant formula and the definition of \(\operatorname {unipotentGL}\): \(\det \begin{pmatrix} 1 & x \\ 0 & 1 \end{pmatrix} = 1\cdot 1 - x \cdot 0 = 1\).

Rewriting with \(\operatorname {lpsMatrixVal_det}\), the determinant equals the sum of squares of the components of \(t\). Since \(t \in \widetilde{S}_p\), we have \(t_0^2 + t_1^2 + t_2^2 + t_3^2 = p\) as integers (from the definition of \(\widetilde{S}_p\)). Applying the ring homomorphism \(\mathbb {Z} \to \mathbb {Z}/q\mathbb {Z}\) and pushing the cast through, we get \(\det = p \in \mathbb {Z}/q\mathbb {Z}\).

Rewriting with \(\operatorname {tupleToGLElement_val}\), the value equals \(\operatorname {lpsMatrixVal}(q,x,y,t)\), and the result follows from \(\operatorname {lpsMatrixVal_det_eq_p}\).

This follows directly by rewriting with \(\operatorname {mem_unipotentSubgroup}\): the membership condition \(g \in \operatorname {unipotentSubgroup}(q)\) is equivalent to the existence of such \(x\).

Suppose \((p : \mathbb {Z}/q\mathbb {Z}) = 0\). By \(\operatorname {ZMod.natCast_eq_zero_iff}\), this means \(q \mid p\). Since \(q\) is prime and \(p\) is prime, the divisibility \(q \mid p\) implies \(q = p\) (as \(p\) is prime, its only divisors are \(1\) and \(p\), and \(q {\gt} 1\)), contradicting \(p \neq q\).

Rewriting with \(\operatorname {jacobiSym.legendreSym.to_jacobiSym}\), the condition \(\operatorname {legendreSym}(q, p) = -1\) becomes \(\operatorname {jacobiSym}(p, q) = -1\). The result then follows from \(\operatorname {ZMod.nonsquare_of_jacobiSym_eq_neg_one}\).

Since \(z\) lies in the center, it commutes with all elements of \(\operatorname {GL}(2,\mathbb {F}_q)\). Let

From \(E_{12} \cdot z.\operatorname {val} = z.\operatorname {val} \cdot E_{12}\), we extract by simplification the \((1,1)\)-entry equation, giving \(z_{10} = 0\), and the \((0,1)\)-entry equation, giving \(z_{00} = z_{11}\). From \(E_{21} \cdot z.\operatorname {val} = z.\operatorname {val} \cdot E_{21}\), we extract the \((0,0)\)-entry equation giving \(z_{01} = 0\). Thus \(z.\operatorname {val}\) is a scalar matrix \(\begin{pmatrix} c & 0 \\ 0 & c \end{pmatrix}\), and \(\det (z.\operatorname {val}) = c^2 = (z_{00})^2\), which is a perfect square.

Suppose for contradiction that \(s \in S_{p,q}\) and \(s \in H\). From \(s \in H\), by \(\operatorname {mem_unipotentSubgroup}\), we obtain \(a \in \mathbb {F}_q\) with \(\operatorname {unipotentPGL}(q,a) = s\). From \(s \in S_{p,q}\), we obtain \(t \in S_p\) (a tuple) such that \(\operatorname {projPGL}(\operatorname {tupleToGLElement}(q,p,\ldots ,t)) = s\).

By \(\operatorname {Sp_subset_SpTilde}\), \(t \in \widetilde{S}_p\). Set

From the equality in \(\operatorname {PGL}\), \(z\) lies in the center of \(\operatorname {GL}(2, \mathbb {F}_q)\). Let \(E_{12}\) and \(E_{21}\) be the elementary matrices from \(\operatorname {matToGL}\). The commutation of \(z\) with \(E_{12}\) and \(E_{21}\) (extracted via the \((1,1)\)-, \((0,1)\)- and \((0,0)\)-entries respectively) shows \(z_{10} = 0\), \(z_{00} = z_{11}\), and \(z_{01} = 0\), so \(\det (z.\operatorname {val}) = (z_{00})^2\).

For the determinant of \(z\): by \(\operatorname {lpsMatrixVal_det_eq_p}\) and \(\operatorname {unipotentGL_det}\), we compute \(\det (z.\operatorname {val}) = (p : \mathbb {F}_q)^{-1}\). Thus \((p : \mathbb {F}_q)^{-1}\) is a perfect square, so by \(\operatorname {isSquare_inv}\), \((p : \mathbb {F}_q)\) is a perfect square. However, by \(\operatorname {not_isSquare_of_legendreSym_neg_one}\), \((p : \mathbb {F}_q)\) is not a square — contradiction.

Suppose \(s = g h g^{-1}\). From \(h \in H\), write \(h = \operatorname {unipotentPGL}(q,a)\) for some \(a\). From \(s \in S_{p,q}\), obtain \(t \in S_p\) with \(\operatorname {projPGL}(\operatorname {tupleToGLElement}(\ldots ,t)) = s\).

Lift \(g\) to a GL element \(G\) via the surjectivity of \(\operatorname {projPGL}\). Then the equality becomes \(\operatorname {projPGL}(\operatorname {tupleToGLElement}(\ldots ,t)) = \operatorname {projPGL}(G \cdot \operatorname {unipotentGL}(q,a) \cdot G^{-1})\) in \(\operatorname {PGL}\). This places \(z := \operatorname {tupleToGLElement}(\ldots ,t)^{-1} \cdot (G \cdot \operatorname {unipotentGL}(q,a) \cdot G^{-1})\) in the center of \(\operatorname {GL}(2, \mathbb {F}_q)\).

By \(\operatorname {center_GL2_det_isSquare}\), \(\det (z.\operatorname {val})\) is a perfect square. We compute \(\det (z.\operatorname {val})\): since \(\det (G \cdot \operatorname {unipotentGL}(q,a) \cdot G^{-1}) = \det (G) \cdot 1 \cdot \det (G^{-1}) = 1\), and \(\det (\operatorname {tupleToGLElement}(\ldots ,t)) = p\) by \(\operatorname {lpsMatrixVal_det_eq_p}\), we get \(\det (z.\operatorname {val}) = p^{-1}\). By \(\operatorname {isSquare_inv}\), \((p : \mathbb {F}_q)\) is a perfect square, contradicting \(\operatorname {not_isSquare_of_legendreSym_neg_one}\).

This follows directly from \(\operatorname {lpsGenSetPGL_satisfiable}\), which provides a witness.

The identity element \(1 \in \operatorname {PGL}(2, \mathbb {F}_q)\) belongs to \(\operatorname {unipotentSubgroup}(q)\) since every subgroup contains the identity.