Suzuki groups from explicit matrix generators

This file defines TauCeti.suzukiGroup n, the Suzuki group usually denoted Sz(2^(2n+1)), as the subgroup of GL₄(𝔽_{2^(2n+1)}) generated by its standard unipotent matrices and a Weyl element. The parameter n = 0 is allowed; it gives the solvable group Sz(2) rather than a finite simple group.

The concrete matrices make this construction suitable for comparison with a fixed-point construction of the Suzuki groups. TauCeti.Suzuki.suzukiGroup_le_iff characterizes containment of the Suzuki group by its generators, so clients need not unfold the subgroup definition.

Main definitions

• TauCeti.Suzuki.unipotent: the standard two-parameter unipotent generators.
• TauCeti.Suzuki.weyl: the standard Weyl generator.
• TauCeti.suzukiGroup: the subgroup generated by these matrices.
• TauCeti.Suzuki.det_eq_one_of_mem_suzukiGroup: every element of a Suzuki group has determinant one.
• TauCeti.Suzuki.unipotentSubgroup: the subgroup U = {u(a, b)} of the unipotent generators, and TauCeti.Suzuki.unipotentSubgroupOf, the same subgroup inside the Suzuki group.
• TauCeti.Suzuki.weylOf: the Weyl generator as an element of the Suzuki group.

Main results

• TauCeti.Suzuki.unipotent_mul_unipotent and TauCeti.Suzuki.unipotent_inv: the unipotent generators multiply by u(a, b) u(c, d) = u(a + c, b + d + a c^θ), with θ = 2^(n+1), and invert by u(a, b)⁻¹ = u(a, b + a^(1+θ)).
• TauCeti.Suzuki.unipotent_pow_four: every unipotent generator has order dividing four.
• TauCeti.Suzuki.unipotent_inj and TauCeti.Suzuki.unipotent_eq_one_iff: a unipotent generator determines its parameters, and is the identity exactly at (0, 0).
• TauCeti.Suzuki.weyl_mul_weyl: the Weyl generator is an involution.
• TauCeti.Suzuki.isPGroup_unipotentSubgroup and TauCeti.Suzuki.isPGroup_unipotentSubgroupOf: the unipotent subgroup is a 2-group.
• TauCeti.Suzuki.exists_pow_two_pow_succ_ne_sq_iff: the generator field has a unit κ with κ^θ ≠ κ^2 exactly when n ≠ 0, so for n ≠ 0 the torus of the Suzuki group acts nontrivially on its unipotent generators.

References

The definitions and determinant computations are adapted from Ryan Smith's Mathlib pull request #42043, commit a1724e1192366aeeee222278c387c06f54213db5.

@[simp]

theorem TauCeti.Suzuki.pow_two_pow_succ_pow_two_pow_succ (n : ℕ) (x : GaloisField 2 (2 * n + 1)) : (x ^ 2 ^ (n + 1)) ^ 2 ^ (n + 1) = x ^ 2

Applying x ↦ x ^ 2 ^ (n + 1) twice on 𝔽_(2^(2n+1)) is the Frobenius x ↦ x ^ 2.

@[simp]

theorem TauCeti.Suzuki.exists_pow_two_pow_succ_ne_sq_iff (n : ℕ) : (∃ (κ : (GaloisField 2 (2 * n + 1))ˣ), ↑κ ^ 2 ^ (n + 1) ≠ ↑κ ^ 2) ↔ n ≠ 0

Some unit κ of 𝔽_(2^(2n+1)) has κ ^ 2 ^ (n + 1) ≠ κ ^ 2 exactly when n ≠ 0; at n = 0 the two exponents agree.

noncomputable def TauCeti.Suzuki.unipotentMatrix (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * n + 1))

The standard unipotent matrix generator of a Suzuki group, over 𝔽_(2^(2n+1)), where x ↦ x ^ 2 ^ (n + 1) is the field endomorphism squaring to the Frobenius.

noncomputable def TauCeti.Suzuki.weylMatrix (n : ℕ) : Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * n + 1))

The standard Weyl generator matrix of a Suzuki group.

@[simp]

theorem TauCeti.Suzuki.unipotentMatrix_apply (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) (i j : Fin 4) : unipotentMatrix n a b i j = ![![1, 0, 0, 0], ![a, 1, 0, 0], ![a * a ^ 2 ^ (n + 1) + b, a ^ 2 ^ (n + 1), 1, 0], ![a ^ 2 * a ^ 2 ^ (n + 1) + a * b + b ^ 2 ^ (n + 1), b, a, 1]] i j

An entry of the standard unipotent generator matrix.

@[simp]

theorem TauCeti.Suzuki.weylMatrix_apply (n : ℕ) (i j : Fin 4) : weylMatrix n i j = ![![0, 0, 0, 1], ![0, 0, 1, 0], ![0, 1, 0, 0], ![1, 0, 0, 0]] i j

An entry of the standard Weyl generator matrix.

@[simp]

theorem TauCeti.Suzuki.det_unipotentMatrix (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : (unipotentMatrix n a b).det = 1

Every standard unipotent generator matrix has determinant one.

@[simp]

theorem TauCeti.Suzuki.det_weylMatrix (n : ℕ) : (weylMatrix n).det = 1

The Weyl generator matrix has determinant one.

noncomputable def TauCeti.Suzuki.unipotent (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : GL (Fin 4) (GaloisField 2 (2 * n + 1))

A standard unipotent generator as an element of the general linear group.

noncomputable def TauCeti.Suzuki.weyl (n : ℕ) : GL (Fin 4) (GaloisField 2 (2 * n + 1))

The standard Weyl generator as an element of the general linear group.

@[simp]

theorem TauCeti.Suzuki.coe_unipotent (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : ↑(unipotent n a b) = unipotentMatrix n a b

The underlying matrix of unipotent n a b is unipotentMatrix n a b.

@[simp]

theorem TauCeti.Suzuki.coe_weyl (n : ℕ) : ↑(weyl n) = weylMatrix n

The underlying matrix of weyl n is weylMatrix n.

@[simp]

theorem TauCeti.Suzuki.unipotent_zero_zero (n : ℕ) : unipotent n 0 0 = 1

The unipotent generator at the parameters (0, 0) is the identity.

@[simp]

theorem TauCeti.Suzuki.unipotent_mul_unipotent (n : ℕ) (a b c d : GaloisField 2 (2 * n + 1)) : unipotent n a b * unipotent n c d = unipotent n (a + c) (b + d + a * c ^ 2 ^ (n + 1))

The multiplication rule of the unipotent generators: u(a, b) u(c, d) = u(a + c, b + d + a c^θ), with θ = 2^(n+1).

theorem TauCeti.Suzuki.unipotent_inv (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : (unipotent n a b)⁻¹ = unipotent n a (b + a * a ^ 2 ^ (n + 1))

The inverse of a unipotent generator: u(a, b)⁻¹ = u(a, b + a^(1+θ)).

@[simp]

theorem TauCeti.Suzuki.unipotent_inj (n : ℕ) {a b c d : GaloisField 2 (2 * n + 1)} : unipotent n a b = unipotent n c d ↔ a = c ∧ b = d

The unipotent generators are determined by their parameters.

@[simp]

theorem TauCeti.Suzuki.unipotent_eq_one_iff (n : ℕ) {a b : GaloisField 2 (2 * n + 1)} : unipotent n a b = 1 ↔ a = 0 ∧ b = 0

A unipotent generator is the identity exactly at the parameters (0, 0).

@[simp]

theorem TauCeti.Suzuki.unipotent_pow_four (n : ℕ) (a b : GaloisField 2 (2 * n + 1)) : unipotent n a b ^ 4 = 1

Every standard unipotent generator has order dividing four.

@[simp]

theorem TauCeti.Suzuki.weyl_mul_weyl (n : ℕ) : weyl n * weyl n = 1

The Weyl generator is an involution.

@[simp]

theorem TauCeti.Suzuki.weyl_inv (n : ℕ) : (weyl n)⁻¹ = weyl n

The Weyl generator is its own inverse.

def TauCeti.Suzuki.generators (n : ℕ) : Set (GL (Fin 4) (GaloisField 2 (2 * n + 1)))

The standard generating set of a Suzuki group.

@[simp]

theorem TauCeti.Suzuki.mem_generators (n : ℕ) {g : GL (Fin 4) (GaloisField 2 (2 * n + 1))} : g ∈ generators n ↔ (∃ (a : GaloisField 2 (2 * n + 1)) (b : GaloisField 2 (2 * n + 1)), g = unipotent n a b) ∨ g = weyl n

An element is a standard generator iff it is a unipotent generator or the Weyl generator.

noncomputable def TauCeti.suzukiGroup (n : ℕ) : Subgroup (GL (Fin 4) (GaloisField 2 (2 * n + 1)))

The Suzuki group Sz(2^(2n+1)), defined by its standard matrix generators.

@[simp]

theorem TauCeti.Suzuki.suzukiGroup_le_iff {n : ℕ} {H : Subgroup (GL (Fin 4) (GaloisField 2 (2 * n + 1)))} : suzukiGroup n ≤ H ↔ (∀ (a b : GaloisField 2 (2 * n + 1)), unipotent n a b ∈ H) ∧ weyl n ∈ H

A subgroup contains the Suzuki group iff it contains every unipotent generator and the Weyl generator.

@[simp]

theorem TauCeti.Suzuki.unipotent_mem_suzukiGroup {n : ℕ} (a b : GaloisField 2 (2 * n + 1)) : unipotent n a b ∈ suzukiGroup n

Every standard unipotent generator belongs to the Suzuki group.

@[simp]

theorem TauCeti.Suzuki.weyl_mem_suzukiGroup {n : ℕ} : weyl n ∈ suzukiGroup n

The standard Weyl generator belongs to the Suzuki group.

theorem TauCeti.Suzuki.det_eq_one_of_mem_suzukiGroup {n : ℕ} {g : GL (Fin 4) (GaloisField 2 (2 * n + 1))} (hg : g ∈ suzukiGroup n) : (↑g).det = 1

A Suzuki group lies in the special linear group: its two families of generating matrices have determinant one, so every element of the group does.

The unipotent subgroup

def TauCeti.Suzuki.unipotentSubgroup (n : ℕ) : Subgroup (GL (Fin 4) (GaloisField 2 (2 * n + 1)))

The unipotent subgroup U = {u(a, b)} of GL₄(𝔽_(2^(2n+1))), consisting of the standard unipotent generators of the Suzuki group.

@[simp]

theorem TauCeti.Suzuki.mem_unipotentSubgroup {n : ℕ} {g : GL (Fin 4) (GaloisField 2 (2 * n + 1))} : g ∈ unipotentSubgroup n ↔ ∃ (a : GaloisField 2 (2 * n + 1)) (b : GaloisField 2 (2 * n + 1)), unipotent n a b = g

The unipotent subgroup consists of the standard unipotent generators.

theorem TauCeti.Suzuki.unipotentSubgroup_le_suzukiGroup (n : ℕ) : unipotentSubgroup n ≤ suzukiGroup n

The unipotent subgroup lies in the Suzuki group.

@[reducible, inline]

noncomputable abbrev TauCeti.Suzuki.unipotentSubgroupOf (n : ℕ) : Subgroup ↥(suzukiGroup n)

The unipotent subgroup U, inside the Suzuki group.

theorem TauCeti.Suzuki.isPGroup_unipotentSubgroup (n : ℕ) : IsPGroup 2 ↥(unipotentSubgroup n)

The unipotent subgroup is a 2-group: each of its elements has order dividing four.

theorem TauCeti.Suzuki.isPGroup_unipotentSubgroupOf (n : ℕ) : IsPGroup 2 ↥(unipotentSubgroupOf n)

The unipotent subgroup is a 2-group inside the Suzuki group.

@[reducible, inline]

noncomputable abbrev TauCeti.Suzuki.weylOf (n : ℕ) : ↥(suzukiGroup n)

The Weyl generator, as an element of the Suzuki group.

@[simp]

theorem TauCeti.Suzuki.weylOf_mul_weylOf (n : ℕ) : weylOf n * weylOf n = 1

The Weyl generator is an involution in the Suzuki group.