Definition 30: Unipotent Subgroup for LPS Graphs #

For the LPS graph X_{p,q} = Cay(PGL(2,q), S_{p,q}), we define the unipotent subgroup H = {[[1,x],[0,1]] | x ∈ 𝔽_q} ⊂ PGL(2,q), which is isomorphic to (𝔽_q, +) ≅ ℤ_q.

Main Definitions #

unipotentGL: The map x ↦ [[1,x],[0,1]] into GL(2, 𝔽_q).
unipotentPGL: The composition with the projection to PGL(2,q).
unipotentSubgroup: The subgroup H ⊂ PGL(2,q).

Main Results #

unipotentPGL_injective: The map x ↦ [[1,x],[0,1]] is injective into PGL.
unipotentSubgroup_card: |H| = q.
lpsGenSet_disjoint_unipotentSubgroup: S_{p,q} ∩ H = ∅.

Unipotent GL elements #

source

def LPS.unipotentGL (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

GL (Fin 2) (ZMod q)

The upper triangular unipotent matrix [[1,x],[0,1]] in GL(2, 𝔽_q).

Equations

LPS.unipotentGL q x = { val := !![1, x; 0, 1], inv := !![1, -x; 0, 1], val_inv := ⋯, inv_val := ⋯ }

Instances For

source

@[simp]

theorem LPS.unipotentGL_val (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

↑(unipotentGL q x) = !![1, x; 0, 1]

source

@[simp]

theorem LPS.unipotentGL_inv_val (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

↑(unipotentGL q x)⁻¹ = !![1, -x; 0, 1]

source

theorem LPS.unipotentGL_zero (q : ℕ) [Fact (Nat.Prime q)] :

unipotentGL q 0 = 1

The unipotent map sends 0 to 1.

source

theorem LPS.unipotentGL_add (q : ℕ) [Fact (Nat.Prime q)] (a b : ZMod q) :

unipotentGL q (a + b) = unipotentGL q a * unipotentGL q b

The unipotent map sends a + b to unipotentGL a * unipotentGL b.

source

def LPS.unipotentPGL (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

PGL2 q

The unipotent element projected to PGL(2,q).

Equations

LPS.unipotentPGL q x = (LPS.projPGL q) (LPS.unipotentGL q x)

Instances For

source

def LPS.unipotentPGLHom (q : ℕ) [Fact (Nat.Prime q)] :

Multiplicative (ZMod q) →* PGL2 q

The map x ↦ [[1,x],[0,1]] as a group homomorphism Multiplicative(ZMod q) →* PGL(2,q).

Equations

LPS.unipotentPGLHom q = { toFun := fun (x : Multiplicative (ZMod q)) => LPS.unipotentPGL q (Multiplicative.toAdd x), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem LPS.unipotentPGLHom_apply (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

(unipotentPGLHom q) (Multiplicative.ofAdd x) = unipotentPGL q x

Injectivity of the unipotent map #

source

theorem LPS.unipotentPGL_injective (q : ℕ) [Fact (Nat.Prime q)] :

Function.Injective (unipotentPGL q)

Two unipotent GL elements that map to the same PGL coset must be equal. If [[1,a],[0,1]] and [[1,b],[0,1]] differ by a scalar in GL, then a = b.

The unipotent subgroup #

source

def LPS.unipotentSubgroup (q : ℕ) [Fact (Nat.Prime q)] :

Subgroup (PGL2 q)

The unipotent subgroup H = {[[1,x],[0,1]] | x ∈ 𝔽_q} ⊂ PGL(2,q). Isomorphic to (𝔽_q, +) ≅ ℤ_q.

Equations

LPS.unipotentSubgroup q = (LPS.unipotentPGLHom q).range

Instances For

source

theorem LPS.mem_unipotentSubgroup (q : ℕ) [Fact (Nat.Prime q)] (g : PGL2 q) :

g ∈ unipotentSubgroup q ↔ ∃ (x : ZMod q), unipotentPGL q x = g

source

instance LPS.instFintypeSubtypePGL2MemSubgroupUnipotentSubgroup (q : ℕ) [Fact (Nat.Prime q)] :

Fintype ↥(unipotentSubgroup q)

Equations

LPS.instFintypeSubtypePGL2MemSubgroupUnipotentSubgroup q = (LPS.unipotentPGLHom q).fintypeRange

source

theorem LPS.unipotentSubgroup_card (q : ℕ) [Fact (Nat.Prime q)] :

Fintype.card ↥(unipotentSubgroup q) = q

The cardinality of the unipotent subgroup is q.

source

theorem LPS.unipotentSubgroup_card_odd (q : ℕ) [Fact (Nat.Prime q)] (hoddq : q % 2 = 1) :

Odd (Fintype.card ↥(unipotentSubgroup q))

The order of H is odd (since q is an odd prime).

Disjointness: S_{p,q} ∩ H = ∅ #

source

@[simp]

theorem LPS.unipotentGL_det (q : ℕ) [Fact (Nat.Prime q)] (x : ZMod q) :

(↑(unipotentGL q x)).det = 1

The determinant of a unipotent GL element is 1.

source

theorem LPS.lpsMatrixVal_det_eq_p (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) :

(lpsMatrixVal q x y t).det = ↑p

The LPS matrix M(a,b,c,d) has determinant a² + b² + c² + d² = p in ZMod q. For (a,b,c,d) ∈ S̃_p, det M = p.

source

theorem LPS.tupleToGLElement_det (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) :

(↑(tupleToGLElement q p hpq x y hxy t ht)).det = ↑p

The determinant of a tupleToGLElement is p (mod q).

source

theorem LPS.unipotentSubgroup_det_is_square (q : ℕ) [Fact (Nat.Prime q)] (g : PGL2 q) (hg : g ∈ unipotentSubgroup q) :

∃ (x : ZMod q), unipotentPGL q x = g

Key lemma: if g ∈ H (unipotent subgroup), then any GL lift of g has determinant that is a perfect square in 𝔽_q^×. Specifically, g = projPGL(unipGL(x)) where det(unipGL(x)) = 1 = 1².

source

theorem LPS.natCast_prime_ne_zero (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) :

↑p ≠ 0

If p ≠ q are primes, then (p : ZMod q) ≠ 0.

source

theorem LPS.not_isSquare_of_legendreSym_neg_one (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hleg : legendreSym q ↑p = -1) :

¬IsSquare ↑↑p

p is not a square in ZMod q when legendreSym q p = -1. Uses ZMod.nonsquare_of_jacobiSym_eq_neg_one via the Legendre-to-Jacobi conversion.

source

theorem LPS.lpsGenSet_disjoint_unipotentSubgroup (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (hleg : legendreSym q ↑p = -1) (s : PGL2 q) :

s ∈ (lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy).carrier → s ∉ unipotentSubgroup q

The generating set S_{p,q} is disjoint from the unipotent subgroup H. This follows because elements of S_{p,q} have determinant p (not a QR mod q), while elements of H have determinant 1 (a QR). In PGL, two GL elements project to the same class iff they differ by a scalar, so their determinants differ by a perfect square. Since (p/q) = -1, p is not a QR — contradiction.

source

theorem LPS.center_GL2_det_isSquare (q : ℕ) [Fact (Nat.Prime q)] (z : GL (Fin 2) (ZMod q)) (hz : z ∈ Subgroup.center (GL (Fin 2) (ZMod q))) :

IsSquare (↑z).det

Elements of the center of GL(2, ZMod q) are scalar matrices, hence have square det.

source

theorem LPS.lpsGenSet_disjoint_conjugate (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (hleg : legendreSym q ↑p = -1) (g s : PGL2 q) (hs : s ∈ (lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy).carrier) (h : PGL2 q) (hh : h ∈ unipotentSubgroup q) :

s ≠ g * h * g⁻¹

The stronger disjointness: S_{p,q} ∩ gHg⁻¹ = ∅ for all g ∈ PGL(2,q). This follows from the determinant argument: conjugation preserves determinant class, so elements of gHg⁻¹ still have determinant class 1, while elements of S_{p,q} have determinant class p ≠ 1 mod squares.

source

theorem LPS.lpsGenSet_disjoint_conjugate_satisfiable :