Dickson's Classification Theorem
Overview
This repository provides a formalisation in the Lean 4 theorem prover of results related to
Dickson's classification theorem for finite subgroups of \text{SL}(2, F) and establishes the
connection of this classification to the classification of \text{PGL}(2, F) over an algebraically closed
field F.
The classification of finite subgroups of linear groups is a classical topic in group theory, with applications to algebraic geometry, representation theory, and number theory. In particular, the original motivation for this project is contribute towards the formalisation of Fermat's Last Theorem as can be seen in the blueprint for the ongoing project FLT
Mathematical Background
The Linear Groups and the Projective Linear Groups
The main object of interest in this repository are the four linear groups:
\text{GL}(n, F), \text{SL}(n, F), \text{PGL}(n, F) and \text{PSL}(n, F)
The General and Special Linear Groups
The general linear group \text{GL}(n, F) is the group of all invertible n \times n matrices
over the field F, with matrix multiplication as the group operation:
\text{GL}(n, F) = \{ A \in M_n(F) \mid \det(A) \neq 0 \}
The special linear group \text{SL}(n, F) is the subgroup of \text{GL}(n, F) consisting of
matrices with determinant equal to 1:
\text{SL}(n, F) = \{ A \in \text{GL}(n, F) \mid \det(A) = 1 \}
The Projective General and Special Linear Groups
The projective general linear group \text{PGL}(n, F) is the quotient of \text{GL}(n, F) by
its center, which consists of scalar matrices \lambda I for \lambda \in F^\times:
\text{PGL}(n, F) = \text{GL}(n, F) / Z(\text{GL}(n, F))
The projective special linear group \text{PSL}(n, F) is the quotient of \text{SL}(n, F) by
its center:
\text{PSL}(n, F) = \text{SL}(n, F) / Z(\text{SL}(n, F))
The center of \text{SL}(n, F) consists of scalar matrices \lambda I where \lambda^n = 1,
i.e., the n-th roots of unity in F.
Reducing the Classification of finite subgroups of PGL₂ to the classification of finite subgroups of SL₂
When working over an algebraically closed field it turns out that \text{PGL}(n, F) is isomorphic to
\text{PSL}(n, F) :
noncomputable def PGL_mulEquiv_PSL (n F : Type*) [Fintype n]
[DecidableEq n] [Field F] [IsAlgClosed F] : PSL n F ≃* PGL n F :=
MulEquiv.ofBijective (PSL_monoidHom_PGL n F) (Bijective_PSL_monoidHom_PGL n F)
Therefore, considering this isomorphism to classify the finite subgroups of \text{PGL}_2(F) over an algebraically closed field
it suffices to classify the finite subgroups of \text{PSL}_2(F). Moreover, since the center of the special linear group is precisely
lemma center_SL2_eq_Z (R : Type*) [CommRing R]
[NoZeroDivisors R] : center SL(2,R) = Z R := R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors R⊢ center SL(2, R) = Z R
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x ∈ center SL(2, R) ↔ x ∈ Z R
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x ∈ center SL(2, R) → x ∈ Z RR:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x ∈ Z R → x ∈ center SL(2, R)
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x ∈ center SL(2, R) → x ∈ Z R R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hx:x ∈ center SL(2, R)⊢ x ∈ Z R
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hx:∃ r, r ^ Fintype.card (Fin 2) = 1 ∧ (scalar (Fin 2)) r = ↑x⊢ x ∈ Z R
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)z:Rz_pow_two_eq_one:z ^ Fintype.card (Fin 2) = 1hz:(scalar (Fin 2)) z = ↑x⊢ x ∈ Z R
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)z:Rhz:(diagonal fun x => z) = ↑xz_pow_two_eq_one:z = 1 ∨ z = -1⊢ x = 1 ∨ x = -1
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ x = 1 ∨ x = -1R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ x = 1 ∨ x = -1
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ x = 1 ∨ x = -1 R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ x = 1
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 0 0 = ↑1 0 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 0 1 = ↑1 0 1R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 1 0 = ↑1 1 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 1 1 = ↑1 1 1 R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 0 0 = ↑1 0 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 0 1 = ↑1 0 1R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 1 0 = ↑1 1 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => 1) = ↑x⊢ ↑x 1 1 = ↑1 1 1 All goals completed! 🐙
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ x = 1 ∨ x = -1 R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ x = -1
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 0 0 = ↑(-1) 0 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 0 1 = ↑(-1) 0 1R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 1 0 = ↑(-1) 1 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 1 1 = ↑(-1) 1 1 R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 0 0 = ↑(-1) 0 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 0 1 = ↑(-1) 0 1R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 1 0 = ↑(-1) 1 0R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)hz:(diagonal fun x => -1) = ↑x⊢ ↑x 1 1 = ↑(-1) 1 1 All goals completed! 🐙
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x ∈ Z R → x ∈ center SL(2, R) R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors Rx:SL(2, R)⊢ x = 1 ∨ x = -1 → x ∈ center SL(2, R)
R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors R⊢ 1 ∈ center SL(2, R)R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors R⊢ -1 ∈ center SL(2, R) R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors R⊢ 1 ∈ center SL(2, R)R:Type u_1inst✝¹:CommRing Rinst✝:NoZeroDivisors R⊢ -1 ∈ center SL(2, R) All goals completed! 🐙
where Z F is defined to be the subgroup of \text{SL}_2(F) generated by -I:
def Z (R : Type*) [CommRing R] : Subgroup SL(2,R) :=
closure {(-1 : SL(2,R))}
If the characteristic of the ring is equal to 2, then the center is isomomorphic to the trivial group
or equivalently, is equal to the bottom subgroup ⊥ : SL(2,F). Therefore, for \text{char}(F) = 2 it follows that
\text{PSL}_2(F) \cong \text{SL}_2(F).
Otherwise, if \text{char}(F) \ne 2 then center contains exactly two elements
and is therefore isomorphic to the cyclic group \mathbb{Z}/2\mathbb{Z}. Thus once finite subgroups of \text{SL}_2(F)
have been classified it should be then straightforward to produce the classification for finite subgroups of \text{PSL}_2(F).
It is for this reason that the focus is shifted towards classifying the finite subgroups of \text{SL}_2(F).
The main characters in this classification are three matrices and the subgroups they generate.
Special Matrices of the Special Linear Group
It turns out that it is sufficient to understand the properties of the following three types of matrices:
The shear matrix
The shear matrix s(\sigma) for \sigma \in F:
def s (σ : F) : SL(2,F) :=
⟨!![1, 0; σ, 1], R:Type uF:Type uinst✝¹:CommRing Rinst✝:Field Fσ:F⊢ !![1, 0; σ, 1].det = 1 All goals completed! 🐙⟩
These matrices form an abelian subgroup under matrix multiplication, satisfying the relation
s(\sigma) \cdot s(\mu) = s(\sigma + \mu):
lemma s_mul_s_eq_s_add (σ μ : F) : s σ * s μ = s (σ + μ) := F:Type uinst✝:Field Fσ:Fμ:F⊢ s σ * s μ = s (σ + μ)
F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 0 0 = ↑(s (σ + μ)) 0 0F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 0 1 = ↑(s (σ + μ)) 0 1F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 1 0 = ↑(s (σ + μ)) 1 0F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 1 1 = ↑(s (σ + μ)) 1 1 F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 0 0 = ↑(s (σ + μ)) 0 0F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 0 1 = ↑(s (σ + μ)) 0 1F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 1 0 = ↑(s (σ + μ)) 1 0F:Type uinst✝:Field Fσ:Fμ:F⊢ ↑(s σ * s μ) 1 1 = ↑(s (σ + μ)) 1 1 All goals completed! 🐙The diagonal matrix
The diagonal matrix d(\delta) for \delta \in F^\times:
def d (δ : Fˣ) : SL(2, F) :=
⟨!![(δ : F), 0; 0 , δ⁻¹], R:Type uF:Type uinst✝¹:CommRing Rinst✝:Field Fδ:Fˣ⊢ !![↑δ, 0; 0, (↑δ)⁻¹].det = 1 All goals completed! 🐙⟩
These matrices form a subgroup isomorphic to F^\times, satisfying the relation
d(\delta) \cdot d(\rho) = d(\delta \rho):
lemma d_mul_d_eq_d_mul (δ ρ : Fˣ) : d δ * d ρ = d (δ * ρ) := F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ d δ * d ρ = d (δ * ρ)
F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 0 0 = ↑(d (δ * ρ)) 0 0F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 0 1 = ↑(d (δ * ρ)) 0 1F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 1 0 = ↑(d (δ * ρ)) 1 0F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 1 1 = ↑(d (δ * ρ)) 1 1 F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 0 0 = ↑(d (δ * ρ)) 0 0F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 0 1 = ↑(d (δ * ρ)) 0 1F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 1 0 = ↑(d (δ * ρ)) 1 0F:Type uinst✝:Field Fδ:Fˣρ:Fˣ⊢ ↑(d δ * d ρ) 1 1 = ↑(d (δ * ρ)) 1 1 All goals completed! 🐙The rotation matrix
The rotation matrix w:
def w : SL(2, F) :=
⟨!![0,1;-1,0], R:Type uF:Type uinst✝¹:CommRing Rinst✝:Field F⊢ !![0, 1; -1, 0].det = 1 All goals completed! 🐙⟩which satisfies:
lemma inv_w_eq_neg_w {F : Type*} [Field F] :
(w : SL(2,F))⁻¹ = - w := F:Type u_1inst✝:Field F⊢ w⁻¹ = -w F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 0 0 = ↑(-w) 0 0F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 0 1 = ↑(-w) 0 1F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 1 0 = ↑(-w) 1 0F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 1 1 = ↑(-w) 1 1 F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 0 0 = ↑(-w) 0 0F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 0 1 = ↑(-w) 0 1F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 1 0 = ↑(-w) 1 0F:Type u_1inst✝:Field F⊢ ↑w⁻¹ 1 1 = ↑(-w) 1 1 All goals completed! 🐙
and in particular, w^4 = I.
Special Subgroups of the Special Linear group
From these matrices it is natural to consider the subgroups of \text{SL}_2(F) generated by these concrete elements.
Later on we will in fact prove that all finite subgroups will be conjugate to one of these subgroups
The subgroup of shear matrices
The subgroup S(F) consists of all shear matrices:
def S (F : Type*) [Field F] : Subgroup SL(2,F) where
carrier := { s σ | σ : F }
mul_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {a b : SL(2, F)}, a ∈ {x | ∃ σ, s σ = x} → b ∈ {x | ∃ σ, s σ = x} → a * b ∈ {x | ∃ σ, s σ = x} F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)Q:SL(2, F)σS:FhσS:s σS = SσQ:FhσQ:s σQ = Q⊢ S * Q ∈ {x | ∃ σ, s σ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)Q:SL(2, F)σS:FhσS:s σS = SσQ:FhσQ:s σQ = Q⊢ s (σS + σQ) = S * Q; All goals completed! 🐙
one_mem' := ⟨0, s_zero_eq_one⟩
inv_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {x : SL(2, F)}, x ∈ {x | ∃ σ, s σ = x} → x⁻¹ ∈ {x | ∃ σ, s σ = x} F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)σ:Fhσ:s σ = S⊢ S⁻¹ ∈ {x | ∃ σ, s σ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)σ:Fhσ:s σ = S⊢ s (-σ) = S⁻¹; All goals completed! 🐙
This subgroup is isomorphic to the additive group of the field F (viewed multiplicatively):
def S_mulEquiv_multiplicative (F : Type*) [Field F]: S F ≃* (Multiplicative F) where
toFun T := T.val 1 0
invFun σ := ⟨s σ, F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ:Multiplicative F⊢ s σ ∈ S F All goals completed! 🐙⟩
left_inv := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ Function.LeftInverse (fun σ => ⟨s σ, ⋯⟩) fun T => ↑↑T 1 0
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ (fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩) = ⟨s, ⋯⟩
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 0 0 = ↑↑⟨s, ⋯⟩ 0 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 0 1 = ↑↑⟨s, ⋯⟩ 0 1F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 1 0 = ↑↑⟨s, ⋯⟩ 1 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 1 1 = ↑↑⟨s, ⋯⟩ 1 1 F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 0 0 = ↑↑⟨s, ⋯⟩ 0 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 0 1 = ↑↑⟨s, ⋯⟩ 0 1F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 1 0 = ↑↑⟨s, ⋯⟩ 1 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs:SL(2, F)σ:Fhσ:SpecialMatrices.s σ = s⊢ ↑↑((fun σ => ⟨SpecialMatrices.s σ, ⋯⟩) ((fun T => ↑↑T 1 0) ⟨s, ⋯⟩)) 1 1 = ↑↑⟨s, ⋯⟩ 1 1 All goals completed! 🐙
right_inv σ := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ:Multiplicative F⊢ (fun T => ↑↑T 1 0) ((fun σ => ⟨s σ, ⋯⟩) σ) = σ All goals completed! 🐙
map_mul' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ (x y : ↥(S F)), ↑↑(x * y) 1 0 = ↑↑x 1 0 * ↑↑y 1 0
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs₁:SL(2, F)σ₁:Fhσ₁:s σ₁ = s₁s₂:SL(2, F)σ₂:Fhσ₂:s σ₂ = s₂⊢ ↑↑(⟨s₁, ⋯⟩ * ⟨s₂, ⋯⟩) 1 0 = ↑↑⟨s₁, ⋯⟩ 1 0 * ↑↑⟨s₂, ⋯⟩ 1 0
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs₁:SL(2, F)σ₁:Fhσ₁:s σ₁ = s₁s₂:SL(2, F)σ₂:Fhσ₂:s σ₂ = s₂⊢ (↑(s σ₁) * ↑(s σ₂)) 1 0 = ↑(s σ₁) 1 0 * ↑(s σ₂) 1 0
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fs₁:SL(2, F)σ₁:Fhσ₁:s σ₁ = s₁s₂:SL(2, F)σ₂:Fhσ₂:s σ₂ = s₂⊢ σ₁ + σ₂ = σ₁ * σ₂
All goals completed! 🐙The subgroup of diagonal matrices
The subgroup D(F) consists of all diagonal matrices of the form d(\delta):
def D (F : Type*) [Field F] : Subgroup SL(2,F) where
carrier := { d δ | δ : Fˣ }
mul_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {a b : SL(2, F)}, a ∈ {x | ∃ δ, d δ = x} → b ∈ {x | ∃ δ, d δ = x} → a * b ∈ {x | ∃ δ, d δ = x} F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)Q:SL(2, F)δS:FˣhδS:d δS = SδQ:FˣhδQ:d δQ = Q⊢ S * Q ∈ {x | ∃ δ, d δ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)Q:SL(2, F)δS:FˣhδS:d δS = SδQ:FˣhδQ:d δQ = Q⊢ d (δS * δQ) = S * Q; All goals completed! 🐙
one_mem' := ⟨1, d_one_eq_one⟩
inv_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {x : SL(2, F)}, x ∈ {x | ∃ δ, d δ = x} → x⁻¹ ∈ {x | ∃ δ, d δ = x} F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)δ:FˣhS:d δ = S⊢ S⁻¹ ∈ {x | ∃ δ, d δ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field FS:SL(2, F)δ:FˣhS:d δ = S⊢ d δ⁻¹ = S⁻¹; All goals completed! 🐙
This subgroup is isomorphic to the multiplicative group of units F:
def D_mulEquiv_units (F : Type*) [Field F] : SpecialSubgroups.D F ≃* Fˣ where
toFun d := ⟨
d.val 0 0,
d.val 1 1,
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)⊢ ↑↑d 0 0 * ↑↑d 1 1 = 1 F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)δ:Fˣhδ:SpecialMatrices.d δ = ↑d⊢ ↑↑d 0 0 * ↑↑d 1 1 = 1; F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)δ:Fˣhδ:SpecialMatrices.d δ = ↑d⊢ ↑(SpecialMatrices.d δ) 0 0 * ↑(SpecialMatrices.d δ) 1 1 = 1; All goals completed! 🐙,
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)⊢ ↑↑d 1 1 * ↑↑d 0 0 = 1 F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)δ:Fˣhδ:SpecialMatrices.d δ = ↑d⊢ ↑↑d 1 1 * ↑↑d 0 0 = 1; F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:↥(D F)δ:Fˣhδ:SpecialMatrices.d δ = ↑d⊢ ↑(SpecialMatrices.d δ) 1 1 * ↑(SpecialMatrices.d δ) 0 0 = 1; All goals completed! 🐙
⟩
invFun δ := ⟨d δ, F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fδ:Fˣ⊢ d δ ∈ D F All goals completed! 🐙⟩
left_inv := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ Function.LeftInverse (fun δ => ⟨d δ, ⋯⟩) fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ (fun δ => ⟨SpecialMatrices.d δ, ⋯⟩) ((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩) =
⟨d, ⋯⟩
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
0 0 =
↑↑⟨d, ⋯⟩ 0 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
0 1 =
↑↑⟨d, ⋯⟩ 0 1F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
1 0 =
↑↑⟨d, ⋯⟩ 1 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
1 1 =
↑↑⟨d, ⋯⟩ 1 1 F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
0 0 =
↑↑⟨d, ⋯⟩ 0 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
0 1 =
↑↑⟨d, ⋯⟩ 0 1F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
1 0 =
↑↑⟨d, ⋯⟩ 1 0F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd:SL(2, F)δ:Fˣhδ:SpecialMatrices.d δ = d⊢ ↑↑((fun δ => ⟨SpecialMatrices.d δ, ⋯⟩)
((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ⟨d, ⋯⟩))
1 1 =
↑↑⟨d, ⋯⟩ 1 1 All goals completed! 🐙
right_inv a := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fa:Fˣ⊢ (fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ((fun δ => ⟨d δ, ⋯⟩) a) = a F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fa:Fˣ⊢ ↑((fun d => { val := ↑↑d 0 0, inv := ↑↑d 1 1, val_inv := ⋯, inv_val := ⋯ }) ((fun δ => ⟨d δ, ⋯⟩) a)) = ↑a; All goals completed! 🐙
map_mul' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ (x y : ↥(D F)),
{ val := ↑↑(x * y) 0 0, inv := ↑↑(x * y) 1 1, val_inv := ⋯, inv_val := ⋯ } =
{ val := ↑↑x 0 0, inv := ↑↑x 1 1, val_inv := ⋯, inv_val := ⋯ } *
{ val := ↑↑y 0 0, inv := ↑↑y 1 1, val_inv := ⋯, inv_val := ⋯ }
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd₁:SL(2, F)δ₁:Fˣhδ₁:d δ₁ = d₁d₂:SL(2, F)δ₂:Fˣhδ₂:d δ₂ = d₂⊢ { val := ↑↑(⟨d₁, ⋯⟩ * ⟨d₂, ⋯⟩) 0 0, inv := ↑↑(⟨d₁, ⋯⟩ * ⟨d₂, ⋯⟩) 1 1, val_inv := ⋯, inv_val := ⋯ } =
{ val := ↑↑⟨d₁, ⋯⟩ 0 0, inv := ↑↑⟨d₁, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ } *
{ val := ↑↑⟨d₂, ⋯⟩ 0 0, inv := ↑↑⟨d₂, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ }
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd₁:SL(2, F)δ₁:Fˣhδ₁:d δ₁ = d₁d₂:SL(2, F)δ₂:Fˣhδ₂:d δ₂ = d₂⊢ ↑↑(⟨d₁, ⋯⟩ * ⟨d₂, ⋯⟩) 0 0 =
↑{ val := ↑↑⟨d₁, ⋯⟩ 0 0, inv := ↑↑⟨d₁, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ } *
↑{ val := ↑↑⟨d₂, ⋯⟩ 0 0, inv := ↑↑⟨d₂, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ }F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd₁:SL(2, F)δ₁:Fˣhδ₁:d δ₁ = d₁d₂:SL(2, F)δ₂:Fˣhδ₂:d δ₂ = d₂⊢ ↑↑(⟨d₁, ⋯⟩ * ⟨d₂, ⋯⟩) 1 1 =
{ val := ↑↑⟨d₂, ⋯⟩ 0 0, inv := ↑↑⟨d₂, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ }.inv *
{ val := ↑↑⟨d₁, ⋯⟩ 0 0, inv := ↑↑⟨d₁, ⋯⟩ 1 1, val_inv := ⋯, inv_val := ⋯ }.inv
repeat'
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fd₁:SL(2, F)δ₁:Fˣhδ₁:d δ₁ = d₁d₂:SL(2, F)δ₂:Fˣhδ₂:d δ₂ = d₂⊢ ↑↑(⟨d δ₁, ⋯⟩ * ⟨d δ₂, ⋯⟩) 1 1 = ↑(d δ₂) 1 1 * ↑(d δ₁) 1 1
All goals completed! 🐙
Another subgroup which will come into play is the pointwise product of S(F) and Z(F):
def SZ (F : Type*) [Field F] : Subgroup SL(2,F) where
carrier := { s σ | σ : F } ∪ { - s σ | σ : F }
mul_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {a b : SL(2, F)},
a ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x} →
b ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x} → a * b ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ₁:Fσ₂:F⊢ s σ₁ * s σ₂ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ₁:Fσ₂:F⊢ s σ₁ * -s σ₂ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ₁:Fσ₂:F⊢ -s σ₁ * s σ₂ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ₁:Fσ₂:F⊢ -s σ₁ * -s σ₂ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}
repeat' All goals completed! 🐙
one_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ 1 ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ s 0 ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}; F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ s 0 ∈ {x | ∃ σ, s σ = x}; All goals completed! 🐙
inv_mem' := F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field F⊢ ∀ {x : SL(2, F)}, x ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x} → x⁻¹ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}
F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ:F⊢ (s σ)⁻¹ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}F✝:Type uinst✝⁴:Field F✝n:Type uinst✝³:Fintype nR:Type uinst✝²:CommRing RG:Type uinst✝¹:Group GF:Type u_1inst✝:Field Fσ:F⊢ (-s σ)⁻¹ ∈ {x | ∃ σ, s σ = x} ∪ {x | ∃ σ, -s σ = x}
repeat' All goals completed! 🐙So far we have defined some very concrete subgroups with no apparent motivation, but we will soon see that understanding properties and interactions of these two family of subgroups alongside the center will allow us to characterise an arbitrary finite subgroup.
Classification of elements of the Special Linear Group up to conjugation
Another neat result concerning elements of \text{SL}_2(F) is that, over an algebraically closed field,
every one of its elements is conjugate to either d(\delta) for some \delta \in F^{\times} or
is conjugate to \pm s(\sigma) for some \sigma \in F:
theorem SL2_isConj_d_or_isConj_s_or_isConj_neg_s_of_algClosed [DecidableEq F] [IsAlgClosed F]
(S : SL(2, F)) :
(∃ δ : Fˣ, IsConj (d δ) S) ∨ (∃ σ : F, IsConj (s σ) S) ∨ (∃ σ : F, IsConj (- s σ) S) := F:Type uinst✝²:Field Finst✝¹:DecidableEq Finst✝:IsAlgClosed FS:SL(2, F)⊢ (∃ δ, IsConj (d δ) S) ∨ (∃ σ, IsConj (s σ) S) ∨ ∃ σ, IsConj (-s σ) SThe subgroup SZ
The subgroup SZ(F) is defined as the join of the shear subgroup S(F) and the center Z(F):
lemma S_sup_Z_eq_SZ : S F ⊔ Z F = SZ F := F:Type uinst✝:Field F⊢ S F ⊔ Z F = SZ F
F:Type uinst✝:Field Fx:SL(2, F)⊢ x ∈ S F ⊔ Z F ↔ x ∈ SZ F
F:Type uinst✝:Field Fx:SL(2, F)⊢ x ∈ S F ⊔ Z F → x ∈ SZ FF:Type uinst✝:Field Fx:SL(2, F)⊢ x ∈ SZ F → x ∈ S F ⊔ Z F
F:Type uinst✝:Field Fx:SL(2, F)⊢ x ∈ S F ⊔ Z F → x ∈ SZ F F:Type uinst✝:Field Fx:SL(2, F)hx:x ∈ S F ⊔ Z F⊢ x ∈ SZ F
F:Type uinst✝:Field Fx:SL(2, F)hx:∀ (K : Subgroup SL(2, F)), ↑(S F) * ↑(Z F) ⊆ ↑K → x ∈ K⊢ x ∈ SZ F
All goals completed! 🐙
F:Type uinst✝:Field Fx:SL(2, F)⊢ x ∈ SZ F → x ∈ S F ⊔ Z F F:Type uinst✝:Field Fσ:F⊢ s σ ∈ S F ⊔ Z FF:Type uinst✝:Field Fσ:F⊢ -s σ ∈ S F ⊔ Z F F:Type uinst✝:Field Fσ:F⊢ s σ ∈ S F ⊔ Z FF:Type uinst✝:Field Fσ:F⊢ -s σ ∈ S F ⊔ Z F F:Type uinst✝:Field Fσ:F⊢ -s σ ∈ Subgroup.closure (↑(S F) * ↑(Z F))
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ Subgroup.closure (↑(S F) * ↑(Z F)) have mem_S_mul_Z : s σ ∈ ((S F) : Set SL(2,F)) * (Z F) := F:Type uinst✝:Field F⊢ S F ⊔ Z F = SZ F
F:Type uinst✝:Field Fσ:F⊢ ∃ x ∈ ↑(S F), ∃ y ∈ ↑(Z F), x * y = s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F) ∧ ∃ y ∈ ↑(Z F), s σ * y = s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F)F:Type uinst✝:Field Fσ:F⊢ ∃ y ∈ ↑(Z F), s σ * y = s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F) F:Type uinst✝:Field Fσ:F⊢ s σ ∈ S F
All goals completed! 🐙
F:Type uinst✝:Field Fσ:F⊢ ∃ y ∈ ↑(Z F), s σ * y = s σ All goals completed! 🐙
All goals completed! 🐙
F:Type uinst✝:Field Fσ:F⊢ -s σ ∈ Subgroup.closure (↑(S F) * ↑(Z F)) have mem_S_mul_Z : -s σ ∈ ((S F) : Set SL(2,F)) * (Z F) := F:Type uinst✝:Field F⊢ S F ⊔ Z F = SZ F
F:Type uinst✝:Field Fσ:F⊢ ∃ x ∈ ↑(S F), ∃ y ∈ ↑(Z F), x * y = -s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F) ∧ ∃ y ∈ ↑(Z F), s σ * y = -s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F)F:Type uinst✝:Field Fσ:F⊢ ∃ y ∈ ↑(Z F), s σ * y = -s σ
F:Type uinst✝:Field Fσ:F⊢ s σ ∈ ↑(S F) F:Type uinst✝:Field Fσ:F⊢ s σ ∈ S F
All goals completed! 🐙
F:Type uinst✝:Field Fσ:F⊢ ∃ y ∈ ↑(Z F), s σ * y = -s σ All goals completed! 🐙
All goals completed! 🐙
An important property is that the centralizer of any non-zero shear matrix s(\sigma) is precisely SZ(F):
theorem centralizer_s_eq_SZ {σ : F} (hσ : σ ≠ 0) : centralizer { s σ } = SZ F := F:Type uinst✝:Field Fσ:Fhσ:σ ≠ 0⊢ centralizer {s σ} = SZ F
Similarly, the centralizer of a diagonal matrix d(\delta) (for \delta \neq 1) is exactly D(F):
lemma centralizer_d_eq_D (δ : Fˣ) (δ_ne_one : δ ≠ 1) (δ_ne_neg_one : δ ≠ -1) :
centralizer {d δ} = D F := F:Type uinst✝:Field Fδ:Fˣδ_ne_one:δ ≠ 1δ_ne_neg_one:δ ≠ -1⊢ centralizer {d δ} = D FFurthermore, given conjugate elements have conjugate centralizers:
lemma conjugate_centralizers_of_isConj (a b : G) (hab : IsConj a b) :
∃ x : G, conj x • (centralizer { a }) = centralizer { b } := G:Type uinst✝:Group Ga:Gb:Ghab:IsConj a b⊢ ∃ x, conj x • centralizer {a} = centralizer {b}
Since every element is conjugate to either \pm s(\sigma) or d(\delta), and the centralizers of these elements are either S(F) \sqcup Z(F) or D(F),
we can conclude that the centralizer of any non-central element of \text{SL}_2(F) is abelian:
lemma isMulCommutative_centralizer_of_not_mem_center [IsAlgClosed F] [DecidableEq F] (x : SL(2,F))
(hx : x ∉ center SL(2,F)) : IsMulCommutative (centralizer { x }) := F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)δ:Fˣx_IsConj_d:IsConj (d δ) x⊢ IsMulCommutative ↥(centralizer {x})F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_s:IsConj (s σ) x⊢ IsMulCommutative ↥(centralizer {x})F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_neg_s:IsConj (-s σ) x⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)δ:Fˣx_IsConj_d:IsConj (d δ) x⊢ IsMulCommutative ↥(centralizer {x}) F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)δ:Fˣx_IsConj_d:IsConj (d δ) xx:SL(2, F)centralizer_x_eq:conj x • centralizer {d δ} = centralizer {x✝}⊢ IsMulCommutative ↥(centralizer {x})
have δ_ne_one : δ ≠ 1 := F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)x_IsConj_d:IsConj (d 1) x✝centralizer_x_eq:conj x • centralizer {d 1} = centralizer {x✝}⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)centralizer_x_eq:conj x • centralizer {d 1} = centralizer {x✝}x_IsConj_d:1 = x✝⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:1 ∉ Z Fx:SL(2, F)centralizer_x_eq:conj x • centralizer {d 1} = centralizer {x✝}x_IsConj_d:1 = x✝⊢ False
All goals completed! 🐙
have δ_ne_neg_one : δ ≠ -1 := F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)x_IsConj_d:IsConj (d (-1)) x✝centralizer_x_eq:conj x • centralizer {d (-1)} = centralizer {x✝}δ_ne_one:-1 ≠ 1⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)centralizer_x_eq:conj x • centralizer {d (-1)} = centralizer {x✝}δ_ne_one:-1 ≠ 1x_IsConj_d:-1 = x✝⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:-1 ∉ Z Fx:SL(2, F)centralizer_x_eq:conj x • centralizer {d (-1)} = centralizer {x✝}δ_ne_one:-1 ≠ 1x_IsConj_d:-1 = x✝⊢ False
All goals completed! 🐙
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)δ:Fˣx_IsConj_d:IsConj (d δ) xx:SL(2, F)centralizer_x_eq:conj x • centralizer {d δ} = centralizer {x✝}δ_ne_one:δ ≠ 1 :=
fun a =>
Eq.ndrec (motive := fun δ => IsConj (d δ) x✝ → conj x • centralizer {d δ} = centralizer {x✝} → False)
(fun x_IsConj_d centralizer_x_eq =>
False.elim
(Eq.mp (Eq.trans (congrArg Not (OneMemClass.one_mem._simp_1 (Z F))) not_true_eq_false)
(Eq.mp (congrArg (fun _a => 1 ∉ _a) (center_SL2_eq_Z F))
(Eq.mp
(congrArg (fun _a => _a ∉ center SL(2, F))
(Eq.symm
(Eq.mp
(Eq.trans
(Eq.trans (congrArg (fun x => IsConj x x✝) d_one_eq_one)
isMulCommutative_centralizer_of_not_mem_center._simp_1)
(Eq.trans
(congrArg Exists
(funext fun c =>
congrArg (fun x => x = x✝)
(Eq.trans (congrArg (fun x => x * c⁻¹) (mul_one c)) (mul_inv_cancel c))))
(isMulCommutative_centralizer_of_not_mem_center._simp_2 SL(2, F))))
x_IsConj_d)))
hx))))
(Eq.symm a) x_IsConj_d centralizer_x_eqδ_ne_neg_one:δ ≠ -1 :=
fun a =>
Eq.ndrec (motive := fun δ => IsConj (d δ) x✝ → conj x • centralizer {d δ} = centralizer {x✝} → δ ≠ 1 → False)
(fun x_IsConj_d centralizer_x_eq δ_ne_one =>
False.elim
(Eq.mp
(Eq.trans
(congrArg Not
(Eq.trans mem_Z_iff._simp_1 (Eq.trans (congrArg (Or (-1 = 1)) (eq_self (-1))) (or_true (-1 = 1)))))
not_true_eq_false)
(Eq.mp (congrArg (fun _a => -1 ∉ _a) (center_SL2_eq_Z F))
(Eq.mp
(congrArg (fun _a => _a ∉ center SL(2, F))
(Eq.symm
(Eq.mp
(Eq.trans
(Eq.trans (congrArg (fun x => IsConj x x✝) d_neg_one_eq_neg_one)
isMulCommutative_centralizer_of_not_mem_center._simp_1)
(Eq.trans
(congrArg Exists
(funext fun c =>
congrArg (fun x => x = x✝)
(Eq.trans
(Eq.trans
(congrArg (fun x => x * c⁻¹) (Eq.trans (mul_neg c 1) (congrArg Neg.neg (mul_one c))))
(neg_mul c c⁻¹))
(congrArg Neg.neg (mul_inv_cancel c)))))
(isMulCommutative_centralizer_of_not_mem_center._simp_2 SL(2, F))))
x_IsConj_d)))
hx))))
(Eq.symm a) x_IsConj_d centralizer_x_eq δ_ne_one⊢ IsMulCommutative ↥(conj x • D F)
All goals completed! 🐙
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_s:IsConj (s σ) x⊢ IsMulCommutative ↥(centralizer {x}) F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_s:IsConj (s σ) xx:SL(2, F)centralizer_S_eq:conj x • centralizer {s σ} = centralizer {x✝}⊢ IsMulCommutative ↥(centralizer {x})
have σ_ne_zero : σ ≠ 0 := F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)x_IsConj_s:IsConj (s 0) x✝centralizer_S_eq:conj x • centralizer {s 0} = centralizer {x✝}⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)centralizer_S_eq:conj x • centralizer {s 0} = centralizer {x✝}x_IsConj_s:1 = x✝⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:1 ∉ Z Fx:SL(2, F)centralizer_S_eq:conj x • centralizer {s 0} = centralizer {x✝}x_IsConj_s:1 = x✝⊢ False
All goals completed! 🐙
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_s:IsConj (s σ) xx:SL(2, F)centralizer_S_eq:conj x • centralizer {s σ} = centralizer {x✝}σ_ne_zero:σ ≠ 0 :=
fun a =>
Eq.ndrec (motive := fun σ => IsConj (s σ) x✝ → conj x • centralizer {s σ} = centralizer {x✝} → False)
(fun x_IsConj_s centralizer_S_eq =>
False.elim
(Eq.mp (Eq.trans (congrArg Not (OneMemClass.one_mem._simp_1 (Z F))) not_true_eq_false)
(Eq.mp (congrArg (fun _a => 1 ∉ _a) (center_SL2_eq_Z F))
(Eq.mp
(congrArg (fun _a => _a ∉ center SL(2, F))
(Eq.symm
(Eq.mp
(Eq.trans
(Eq.trans (congrArg (fun x => IsConj x x✝) s_zero_eq_one)
isMulCommutative_centralizer_of_not_mem_center._simp_1)
(Eq.trans
(congrArg Exists
(funext fun c =>
congrArg (fun x => x = x✝)
(Eq.trans (congrArg (fun x => x * c⁻¹) (mul_one c)) (mul_inv_cancel c))))
(isMulCommutative_centralizer_of_not_mem_center._simp_2 SL(2, F))))
x_IsConj_s)))
hx))))
(Eq.symm a) x_IsConj_s centralizer_S_eq⊢ IsMulCommutative ↥(conj x • SZ F)
All goals completed! 🐙
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_neg_s:IsConj (-s σ) x⊢ IsMulCommutative ↥(centralizer {x}) F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_neg_s:IsConj (-s σ) xx:SL(2, F)centralizer_S_eq:conj x • centralizer {-s σ} = centralizer {x✝}⊢ IsMulCommutative ↥(centralizer {x})
have σ_ne_zero : σ ≠ 0 := F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx:SL(2, F)hx:x ∉ center SL(2, F)⊢ IsMulCommutative ↥(centralizer {x})
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)x_IsConj_neg_s:IsConj (-s 0) x✝centralizer_S_eq:conj x • centralizer {-s 0} = centralizer {x✝}⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)x:SL(2, F)centralizer_S_eq:conj x • centralizer {-s 0} = centralizer {x✝}x_IsConj_neg_s:-1 = x✝⊢ False
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:-1 ∉ Z Fx:SL(2, F)centralizer_S_eq:conj x • centralizer {-s 0} = centralizer {x✝}x_IsConj_neg_s:-1 = x✝⊢ False
All goals completed! 🐙
F:Type uinst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fx✝:SL(2, F)hx:x ∉ center SL(2, F)σ:Fx_IsConj_neg_s:IsConj (-s σ) xx:SL(2, F)centralizer_S_eq:conj x • centralizer {-s σ} = centralizer {x✝}σ_ne_zero:σ ≠ 0 :=
fun a =>
Eq.ndrec (motive := fun σ => IsConj (-s σ) x✝ → conj x • centralizer {-s σ} = centralizer {x✝} → False)
(fun x_IsConj_neg_s centralizer_S_eq =>
False.elim
(Eq.mp
(Eq.trans
(congrArg Not
(Eq.trans mem_Z_iff._simp_1 (Eq.trans (congrArg (Or (-1 = 1)) (eq_self (-1))) (or_true (-1 = 1)))))
not_true_eq_false)
(Eq.mp (congrArg (fun _a => -1 ∉ _a) (center_SL2_eq_Z F))
(Eq.mp
(congrArg (fun _a => _a ∉ center SL(2, F))
(Eq.symm
(Eq.mp
(Eq.trans
(Eq.trans (congrArg (fun x => IsConj (-x) x✝) s_zero_eq_one)
isMulCommutative_centralizer_of_not_mem_center._simp_1)
(Eq.trans
(congrArg Exists
(funext fun c =>
congrArg (fun x => x = x✝)
(Eq.trans
(Eq.trans
(congrArg (fun x => x * c⁻¹) (Eq.trans (mul_neg c 1) (congrArg Neg.neg (mul_one c))))
(neg_mul c c⁻¹))
(congrArg Neg.neg (mul_inv_cancel c)))))
(isMulCommutative_centralizer_of_not_mem_center._simp_2 SL(2, F))))
x_IsConj_neg_s)))
hx))))
(Eq.symm a) x_IsConj_neg_s centralizer_S_eq⊢ IsMulCommutative ↥(conj x • SZ F)
All goals completed! 🐙This fact will foreshadow a result to come, namely, how most maximal abelian subgroups arise are the centralizers of non-central elements.
The Maximal Abelian Subgroup Class Equation
In order to use the classification of elements of \text{SL}_2(F) up to conjugacy for the desired finite subgroup classification theorem, we must
first define the notion of a maximal abelian subgroup of a particular subgroup.
Maximal abelian subgroups of a subgroup
First we must define the notion of maximal abelian subgroup, namely:
def IsMaximalAbelian {L : Type*} [Group L] (G : Subgroup L) : Prop :=
Maximal (P := fun (K : Subgroup L) => IsMulCommutative K) Gand from this definition we are ready to define the set of maximal abelian subgroups of a subgroup:
def MaximalAbelianSubgroupsOf { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
{ K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}
Altogether, given conjugate elements have conjugate centralizers, every element is conjugate to either d(\delta) or s(\sigma),
the centralizer of this element is conjugate to a commutative subgroup, thus is commutative; and furthermore, it can be shown to be maximal.
We can conclude that the centralizer of an arbitrary element restricted to G$ is a maximal abelian subgroup of G.
theorem centralizer_inf_mem_maximalAbelianSubgroupsOf_of_noncentral {F : Type*} [Field F]
[IsAlgClosed F] [DecidableEq F] (G : Subgroup SL(2,F)) (x : SL(2,F))
(hx : x ∈ (G.carrier \ (center SL(2,F)))) :
centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G := F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F))⊢ centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ ↑(center SL(2, F))⊢ centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)⊢ centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ IsMaximalAbelian ((centralizer {x} ⊓ G).subgroupOf G) ∧ centralizer {x} ⊓ G ≤ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ (fun K => IsMulCommutative ↥K) ((centralizer {x} ⊓ G).subgroupOf G)F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ ∀ ⦃y : Subgroup ↥G⦄,
(fun K => IsMulCommutative ↥K) y → (centralizer {x} ⊓ G).subgroupOf G ≤ y → y ≤ (centralizer {x} ⊓ G).subgroupOf GF:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ centralizer {x} ⊓ G ≤ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ (fun K => IsMulCommutative ↥K) ((centralizer {x} ⊓ G).subgroupOf G) F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ (fun K => IsMulCommutative ↥K) ((centralizer {x}).subgroupOf G)
All goals completed! 🐙
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_Z⊢ ∀ ⦃y : Subgroup ↥G⦄,
(fun K => IsMulCommutative ↥K) y → (centralizer {x} ⊓ G).subgroupOf G ≤ y → y ≤ (centralizer {x} ⊓ G).subgroupOf G F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ j ∈ (centralizer {x} ⊓ G).subgroupOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ ∀ h ∈ {x}, h * ↑j = ↑j * h
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x * ↑j = ↑j * x
have x_in_J : ⟨x, x_in_G⟩ ∈ J := F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F))⊢ centralizer {x} ⊓ G ∈ MaximalAbelianSubgroupsOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ ⟨x, x_in_G⟩ ∈ (centralizer {x} ⊓ G).subgroupOf G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ ↑⟨x, x_in_G⟩ ∈ centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x ∈ centralizer {x} ∧ x ∈ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x ∈ centralizer {x}F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x ∈ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x ∈ centralizer {x} All goals completed! 🐙
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ J⊢ x ∈ G All goals completed! 🐙
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FG:Subgroup SL(2, F)x:SL(2, F)x_in_G:x ∈ G.carrierx_not_in_Z:x ∉ center SL(2, F)IsMulCommutative_centralizer_S:IsMulCommutative ↥(centralizer {x}) := isMulCommutative_centralizer_of_not_mem_center x x_not_in_ZJ:Subgroup ↥GhJ:IsMulCommutative ↥Jhx:(centralizer {x} ⊓ G).subgroupOf G ≤ Jj:↥Gj_in_J:j ∈ Jx_in_J:⟨x, x_in_G⟩ ∈ J :=
hx
(mem_subgroupOf.mpr
(Eq.mpr (id centralizer_inf_mem_maximalAbelianSubgroupsOf_of_noncentral._simp_3) ⟨mem_centralizer_self x, x_in_G⟩))this:⟨x, x_in_G⟩ * j = j * ⟨x, x_in_G⟩ := mul_comm_of_mem_isMulCommutative J x_in_J j_in_J⊢ x * ↑j = ↑j * x
All goals completed! 🐙
All goals completed! 🐙
In fact, we can go even further and say that maximal abelian subgroups of G arise as the centralizer of a non-central element
restricted to G.
lemma eq_centralizer_inf_of_center_lt {F : Type*} [Field F] [IsAlgClosed F] [DecidableEq F]
(A G : Subgroup SL(2,F)) (center_lt : center SL(2,F) < A) (hA : A ∈ MaximalAbelianSubgroupsOf G) :
∃ x : SL(2,F), x ∈ G.carrier \ center SL(2,F) ∧ A = centralizer {x} ⊓ G := F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)center_lt:center SL(2, F) < AhA:A ∈ MaximalAbelianSubgroupsOf G⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)center_lt:center SL(2, F) ≤ A ∧ ∃ x ∈ A, x ∉ center SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf G⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_center⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_centercentra_meet_G_IsComm:IsMulCommutative ↥((centralizer {x} ⊓ G).subgroupOf G)⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
/- We show centralizer {x} ⊓ G ≤ A -/
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_centercentra_meet_G_IsComm:IsMulCommutative ↥((centralizer {x} ⊓ G).subgroupOf G)A_le_centralizer_meet_G:A ≤ centralizer {x} ⊓ G := le_centralizer_meet A G hA x x_in_A⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
have A_le_centralizer_meet_G' : A.subgroupOf G ≤ (centralizer {x} ⊓ G).subgroupOf G := F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)center_lt:center SL(2, F) < AhA:A ∈ MaximalAbelianSubgroupsOf G⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_centercentra_meet_G_IsComm:IsMulCommutative ↥((centralizer {x} ⊓ G).subgroupOf G)A_le_centralizer_meet_G:A ≤ centralizer {x} ⊓ G := le_centralizer_meet A G hA x x_in_A⊢ A ⊓ G ≤ centralizer {x}
All goals completed! 🐙
/- using the maximality of A and using the fact A ≤ centralizer {x} ⊓ G -/
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_centercentra_meet_G_IsComm:IsMulCommutative ↥((centralizer {x} ⊓ G).subgroupOf G)A_le_centralizer_meet_G:A ≤ centralizer {x} ⊓ G := le_centralizer_meet A G hA x x_in_AA_le_centralizer_meet_G':A.subgroupOf G ≤ (centralizer {x} ⊓ G).subgroupOf G :=
Eq.mpr
(id
(Eq.trans
(Eq.trans (congrArg (LE.le (A.subgroupOf G)) (inf_subgroupOf_right (centralizer {x}) G)) center_le._simp_1)
(Eq.trans
(Eq.trans (congr (congrArg LE.le (subgroupOf_map_subtype A G)) (subgroupOf_map_subtype (centralizer {x}) G))
center_eq_meet_of_ne_MaximalAbelianSubgroups._simp_1)
(Eq.trans (congrArg (And (A ⊓ G ≤ centralizer {x})) center_eq_meet_of_ne_MaximalAbelianSubgroups._simp_2)
(and_true (A ⊓ G ≤ centralizer {x}))))))
(le_trans inf_le_left (le_trans A_le_centralizer_meet_G inf_le_left))centralizer_meet_G_le_A:(centralizer {x} ⊓ G).subgroupOf G ≤ A.subgroupOf G := hA.left.right centra_meet_G_IsComm A_le_centralizer_meet_G'⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq FA:Subgroup SL(2, F)G:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gx:SL(2, F)x_in_A:x ∈ Ax_not_in_center:x ∉ center SL(2, F)hx:x ∈ G.carrier \ ↑(center SL(2, F)) := Set.mem_diff_of_mem (hA.right x_in_A) x_not_in_centercentra_meet_G_IsComm:IsMulCommutative ↥((centralizer {x} ⊓ G).subgroupOf G)A_le_centralizer_meet_G:A ≤ centralizer {x} ⊓ G := le_centralizer_meet A G hA x x_in_AA_le_centralizer_meet_G':A.subgroupOf G ≤ (centralizer {x} ⊓ G).subgroupOf G :=
Eq.mpr
(id
(Eq.trans
(Eq.trans (congrArg (LE.le (A.subgroupOf G)) (inf_subgroupOf_right (centralizer {x}) G)) center_le._simp_1)
(Eq.trans
(Eq.trans (congr (congrArg LE.le (subgroupOf_map_subtype A G)) (subgroupOf_map_subtype (centralizer {x}) G))
center_eq_meet_of_ne_MaximalAbelianSubgroups._simp_1)
(Eq.trans (congrArg (And (A ⊓ G ≤ centralizer {x})) center_eq_meet_of_ne_MaximalAbelianSubgroups._simp_2)
(and_true (A ⊓ G ≤ centralizer {x}))))))
(le_trans inf_le_left (le_trans A_le_centralizer_meet_G inf_le_left))centralizer_meet_G_le_A:centralizer {x} ⊓ G ≤ A⊢ ∃ x ∈ G.carrier \ ↑(center SL(2, F)), A = centralizer {x} ⊓ G
/- We show A = centralizer {x} ⊓ G -/
All goals completed! 🐙
Provided this correspondence between maximal abelian subgroups of G and centralizers of non-central elements of \text{SL}_2(F) it is possible
to classify maximal abelian subgroups as one of two cases:
theorem isCyclic_and_card_coprime_charP_or_eq_Q_sup_Z {F : Type*}
[Field F] [IsAlgClosed F] [DecidableEq F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p]
(G : Subgroup SL(2, F)) [hG₀ : Finite ↥G] (A : Subgroup SL(2, F))
(hA : A ∈ MaximalAbelianSubgroupsOf G) (center_le_G : center SL(2, F) ≤ G) :
IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p
∨
∃ Q : Subgroup SL(2,F),
Nontrivial Q ∧ Finite Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧
IsElementaryAbelian p Q ∧ ∃ S : Sylow p G, Q.subgroupOf G = S := F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ G⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_eq_G:G = center SL(2, F)⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑SF:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
case inl F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_eq_G:G = center SL(2, F)⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_eq_G:G = center SL(2, F)⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p
All goals completed! 🐙
case inr F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₁:(Nat.card ↥A).Coprime ph₂:IsCyclic ↥A⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑SF:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₃:∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₁:(Nat.card ↥A).Coprime ph₂:IsCyclic ↥A⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₁:(Nat.card ↥A).Coprime ph₂:IsCyclic ↥A⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p
All goals completed! 🐙
F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₃:∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S⊢ IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨
∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S F:Type u_1inst✝²:Field Finst✝¹:IsAlgClosed Finst✝:DecidableEq Fp:ℕhp':Fact (Nat.Prime p)hC:CharP F pG:Subgroup SL(2, F)hG₀:Finite ↥GA:Subgroup SL(2, F)hA:A ∈ MaximalAbelianSubgroupsOf Gcenter_le_G:center SL(2, F) ≤ Gcenter_ne_G:G ≠ center SL(2, F)h₃:∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S⊢ ∃ Q, Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ Z F ∧ IsElementaryAbelian p Q ∧ ∃ S, Q.subgroupOf G = ↑S
All goals completed! 🐙Elementary Abelian Subgroups
A subgroup H is called elementary abelian of exponent p if it is abelian and every
non-identity element has order p:
def IsElementaryAbelian {G : Type*} [Group G] (p : ℕ) (H : Subgroup G) : Prop :=
IsMulCommutative H ∧ ∀ h : H, h ≠ 1 → orderOf h = pDickson's Classification Theorem
Main Theorem Structure
The classification divides finite subgroups of \text{SL}(2, F) into several cases based on
the relationship between the group and its Sylow p-subgroups, where p is the
characteristic of the field.
Classification for Characteristic Coprime Groups
When the order of G is coprime to the characteristic p of the field:
theorem dicksons_classification_theorem_class_I {F : Type*} [Field F] [IsAlgClosed F]
{p : ℕ} [CharP F p] (hp : Prime p) (G : Subgroup (SL(2,F))) [Finite G]
(hp' : p = 0 ∨ Nat.Coprime (Nat.card G) p) :
IsCyclic G ∨
Isomorphic G (DihedralGroup n)
∨
Isomorphic G SL(2, ZMod 3)
∨
Isomorphic G SL(2, ZMod 5)
∨
Isomorphic G (GL (Fin 2) (ZMod 3))
:= n:ℕ+F:Type u_1inst✝³:Field Finst✝²:IsAlgClosed Fp:ℕinst✝¹:CharP F php:Prime pG:Subgroup SL(2, F)inst✝:Finite ↥Ghp':p = 0 ∨ (Nat.card ↥G).Coprime p⊢ IsCyclic ↥G ∨
Isomorphic (↥G) (DihedralGroup ↑n) ∨
Isomorphic ↥G SL(2, ZMod 3) ∨ Isomorphic ↥G SL(2, ZMod 5) ∨ Isomorphic (↥G) (GL (Fin 2) (ZMod 3)) All goals completed! 🐙Classification for Characteristic Dividing Groups
When the characteristic p divides the order of the group:
theorem dicksons_classification_theorem_class_II {F : Type*} [Field F] [IsAlgClosed F]{p : ℕ}
[Fact (Nat.Prime p)] [CharP F p] (G : Subgroup (SL(2,F))) [Finite G] (hp : p ∣ Nat.card G) :
∃ Q : Subgroup SL(2,F), IsElementaryAbelian p Q ∧ Normal Q ∧ Isomorphic G Q
∨
(p = 2 ∧ ∃ n : ℕ, Odd n ∧ Isomorphic G (DihedralGroup n))
∨
Isomorphic G SL(2, ZMod 5)
∨
∃ k : ℕ+, Isomorphic G SL(2, GaloisField p k)
∨
∃ k : ℕ+, ∃ x : GaloisField p (2* k), orderOf x^2 = p^(k : ℕ) ∧
∃ φ : G ≃* SL(2, GaloisField p k), True
:= F:Type u_1inst✝⁴:Field Finst✝³:IsAlgClosed Fp:ℕinst✝²:Fact (Nat.Prime p)inst✝¹:CharP F pG:Subgroup SL(2, F)inst✝:Finite ↥Ghp:p ∣ Nat.card ↥G⊢ ∃ Q,
IsElementaryAbelian p Q ∧ Q.Normal ∧ Isomorphic ↥G ↥Q ∨
(p = 2 ∧ ∃ n, Odd n ∧ Isomorphic (↥G) (DihedralGroup n)) ∨
Isomorphic ↥G SL(2, ZMod 5) ∨
∃ k, Isomorphic ↥G SL(2, GaloisField p ↑k) ∨ ∃ k x, orderOf x ^ 2 = p ^ ↑k ∧ ∃ φ, True All goals completed! 🐙Classification for PGL₂
The classification extends to finite subgroups of \text{PGL}(2, \overline{\mathbb{F}_p}):
theorem FLT_classification_fin_subgroups_of_PGL2_over_AlgClosure_ZMod {p : ℕ}
[Fact (Nat.Prime p)] (𝕂 : Type*) [Field 𝕂] [CharP 𝕂 p] [Finite 𝕂]
(G : Subgroup (PGL (Fin 2) (AlgebraicClosure (ZMod p)))) [hG : Finite G] :
IsCyclic G
∨
∃ n, Isomorphic G (DihedralGroup n)
∨
Isomorphic G (alternatingGroup (Fin 4))
∨
Isomorphic G (Equiv.Perm (Fin 5))
∨
Isomorphic G (alternatingGroup (Fin 5))
∨
Isomorphic G (PSL (Fin 2) (𝕂))
∨
Isomorphic G (PGL (Fin 2) (𝕂)) := p:ℕinst✝³:Fact (Nat.Prime p)𝕂:Type u_3inst✝²:Field 𝕂inst✝¹:CharP 𝕂 pinst✝:Finite 𝕂G:Subgroup (PGL (Fin 2) (AlgebraicClosure (ZMod p)))hG:Finite ↥G⊢ IsCyclic ↥G ∨
∃ n,
Isomorphic (↥G) (DihedralGroup n) ∨
Isomorphic ↥G ↥(alternatingGroup (Fin 4)) ∨
Isomorphic (↥G) (Equiv.Perm (Fin 5)) ∨
Isomorphic ↥G ↥(alternatingGroup (Fin 5)) ∨ Isomorphic (↥G) (PSL (Fin 2) 𝕂) ∨ Isomorphic (↥G) (PGL (Fin 2) 𝕂)
All goals completed! 🐙Repository Structure
The repository is organised as follows:
-
Lean/Dicksons The formal Lean 4 proofs, including:
-
Ch4_PGLIsoPSLOverAlgClosedField/: Establishes the isomorphism between PGL and PSL over algebraically closed fields -
Ch5_PropertiesOfSLOverAlgClosedField/: Properties of SL₂ including special matrices and subgroups -
Ch6_MaximalAbelianSubgroupClassEquation/: Maximal abelian subgroups and class equations -
Ch7_DicksonsClassificationTheorem.lean: The main classification theorem
-
-
Verso Lean code for generating this documentation website using the Verso framework.
-
site Jekyll website source files, completed by the Verso-generated content.
References
-
Dickson, L.E. (1901). "Linear Groups with an Exposition of the Galois Field Theory". Teubner, Leipzig.
-
Suzuki, M. (1982). "Group Theory I". Grundlehren der mathematischen Wissenschaften, vol. 247, Springer-Verlag.
-
Huppert, B. (1967). "Endliche Gruppen I". Grundlehren der mathematischen Wissenschaften, vol. 134, Springer-Verlag.