classification of finite subgroups of SL(2,F)

Stream: maths

[Alex Brodbelt]

Edit:

Context:

I am working on the classification of finite subgroups of $\textrm{SL}(2, F)$, where $F$ is an algebraically closed field of characteristic $p$.

This is relevant because $\textrm{PSL}(2,F) \cong \textrm{PGL}(2,F)$ when $F$ is algebraically closed, and it should not be too much work to classify subgroups of $\textrm{PSL}(2,F)$ from $\textrm{SL}(2,F)$ considering the center is $\langle -I \rangle$.

I am primarily following:
ChristopherButlerExpositionOnClassificationFinSubSL2F
as a lot of the works is done for me, most if not all proofs are there.

So far I have formalised Chapter 1 - Properties of SL(2, F) over an Algebraically Closed Field.

Summarising the main definitions and results:

Definitions:

• $d_\delta = \begin{pmatrix}\delta & 0\\0 & \delta^{-1}\end{pmatrix}$

• $t_\tau = \begin{pmatrix}1 & 0\\\tau & 1\end{pmatrix}$ (will be renamed after Kevin's comment)

• $D = \{d_\delta | \delta \in F^{\times} \}$

• $T = \{t_\tau | \tau \in F\}$ (will probably be renamed after Kevin's comment)
• $Z = Z(\textrm{SL}(2,F))$
• $G$ is a finite subgroup of $\textrm{SL}(2,F)$, which is the object to be classified.

Main results:

• An element $x$ of $\textrm{SL}(2,F)$ is conjugate to either $d_\delta$ or $\pm t_\tau$. (1)

• $D \cong F^{\times}$. (2)

• $T \cong F$ (additive group within $F$). (3)

• $C_{\textrm{SL(2,F)}}(d_\delta) = D$ for $\delta \neq 1, -1$.

• $C_{\textrm{SL(2,F)}}(\pm t_\tau) = T \sqcup Z = T\cdot Z$ for $\tau \neq 0$.

• Conjugate elements have conjugate centralizers. (4)

• $C_{\textrm{SL(2,F)}}(x)$ is commutative (using (1), (4) and (2) (3) ).

• Results on normalizers of $T_0 \leq T$ and $D_0 \leq D$.

Chapter 2 - The Maximal Abelian Subgroup Class Equation

Definitions:

• $M$ is the set of maximal abelian subgroups of $G$. Implemented as:

def IsMaximalAbelian (G : Type*) [Group G] (H : Subgroup G) : Prop := Maximal (IsCommutative) H

def MaximalAbelianSubgroups { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
  { K : Subgroup L | IsMaximalAbelian G (K.subgroupOf G) ∧ K ≤ G}

• Elementary Abelian Subgroups. I am aware Yaël mentioned that they were defined in PFR but were defined additively. I have defined them as a simple proposition:

def IsElementaryAbelian {G : Type*} [Group G] (p : ℕ) (H : Subgroup G) : Prop :=
  IsCommutative H ∧ ∀ h : H, h ≠ 1 → orderOf h = p

Main results:

• If $x \in G \setminus Z$ then $C_G(x) = C_{\textrm{SL(2,F)}} \sqcap G \in M$.

• If $A, B \in M$ and $A \neq B$ then $A \sqcap B = Z$.

• If $A \in M$ either $A$ is cyclic and has order coprime to $p = \textrm{char}(F)$ or it is isomorphic to $Q \sqcup Z$ where $Q$ is elementary abelian $p$-Sylow subgroup of $G$ (Currently on this one, half way there or so, after Artie's idea I think I will done with this today).

---

(This is for proving Theorem 2.3.iii in the exposition which is available above)

Let

• $F$ be a field of characteristic $p$, the exposition does not treat the case when $p = 0$ as far as I can see (even though it seems to assume it has been proven for this case).
• $G$ a finite subgroup of $\textrm{SL}(2,F)$ containing the center ; G :SL(2,F) with center SL(2,F) = Z < G (explicitly, $Z \neq G$ - the case where they are equal has been treated).
• $A$ be a maximal abelian subgroup of $G$ has type A : Subgroup Subgroup SL(2,F) with A ≤ G.

Then $A$ is either cyclic and has order coprime to $p = \textrm{char}(F)$ or it is isomorphic to $Q \sqcup Z$ where $Q$ is elementary abelian $p$-Sylow subgroup of $G$.

proof/formalization/sketch:

As $Z < A$ there exists an element $x \in A \subseteq G \setminus Z$, such that $C_G(x) = A$.

As $x$ is conjugate to $d_\delta$ or $\pm t_\tau$, (the case where $x$ is conjugate to $d_\delta$ has been dealt with after help from Kevin and others in another thread) so we focus on the case where $x$ is conjugate to $t_\tau$ (the case for $-t_\tau$ is exactly the same so we leave it).

There exists some $\tau \neq 0$ (as otherwise, if $\tau = 0$, $x = 1_{\textrm{SL(2,F)}} \in Z$) such that $x$ is conjugate to $t_\tau$; because conjugate elements have conjugate centralizers, there exists some $c \in \textrm{SL(2,F)}$ such that $A = C_G(x) = C_{\textrm{SL(2,F)}}(x) \sqcap G =c^{-1} C_{\textrm{SL}(2,F)}(t_\tau) c \sqcap G$.

Bearing in mind, $C_{\textrm{SL}(2,F)}(t_\tau) = T \cdot Z = T \sqcup Z \cong T \times Z$ and taking into account Artie's reasoning.

$c^{-1} C_{\textrm{SL}(2,F)}(t_\tau) c \sqcap G = (c^{-1}T Z c)\sqcap G = (c^{−1}Tc⋅Z)\sqcap G = (c^{−1}Tc \sqcap G) \sqcup Z \cong (T \sqcap cGc^{-1} )\sqcup Z$.

The last isomorphism is constructed by feeding in one isomorphism into another:
From the isomorphism $c^{−1}Tc\sqcap G\cong T\sqcap cGc^{−1}$ and $A \sqcup Z = B \sqcup Z$ for $A \cong B$, $Z$ normal (as commutative) and trivial intersection between $Z \sqcap A = \{1\} = Z \sqcap B$. this is what I am stuck trying to formalize

All of this allows to conclude $A \cong (T \sqcap cGc^{-1} \sqcup Z$, denote the isomorphism by$$\phi$$. Because $G$ is finite $c G c^{-1}$ is finite and pulling back $T \sqcap cGc^{-1}$ along $\phi$ is the desired $Q =: \phi^{-1} (T \sqcap cGc^{-1})$ as I believe $\phi^{-1} (Z) = Z$.

Assuming this last part is correct, then for characteristic $p$ take $q \in Q$, then as $q \in T$, there must exist $\tau'$ such that $t_{\tau'} = q$ and $q^p = 1$, this was arbitrary for any $q \in Q$ so this fact added with $Q$ being commutative, we can conclude $Q$ is elementary abelian.

...It being $p$-Sylow subgroup can wait for now.

Thank you for the help so far, and thank you in advance.

[Artie Khovanov]

I'm a bit confused about what you're assuming and what you're trying to prove, but I'll try my best. Since $Z$ commutes with everything, we have

$A=(c^{-1}TZc)\cap G=(c^{-1}Tc\cdot Z)\cap G=(c^{-1}Tc\cap G)Z.$

So it's enough to show that $c^{-1}Tc\cap G\cong T\cap cGc^{-1}$ is elementary abelian.

Now, I think you've told me you can prove that $T_0=T\cap G$ is elementary abelian. If you do this proof with $G$ replaced by $cGc^{-1}$, which is also a subgroup containing the centre, then you're done.

Sorry if I made a wrong assumption somewhere!

[Alex Brodbelt]

Ooh! this could work

[Alex Brodbelt]

also I think I'll rename this thread in case I have more questions about stuff in my particular project and so there is more context for people.

[Alex Brodbelt]

thanks @Artie Khovanov ! :)

[Artie Khovanov]

Also - aren't all subgroups of $\text{SL}_2(F)$ finite?

[Artie Khovanov]

I assumed $F$ was a finite field. Is it just any char $p$ field? Doesn't change my idea above, but

[Alex Brodbelt]

yes its for any characteristic, and I'm pretty sure your idea works - will come back with formalization of it.

[Kevin Buzzard]

One problem with this thread is that it just launches into a wall of maths without giving any definitions. This just leads to confusion. Alex can you tell us what F is? It would be nice if the question was self-contained rather than just assuming everyone has remembered you're previous questions

[Alex Brodbelt]

$F$ is an algebraically closed field

[Kevin Buzzard]

Another thing I find quite jarring is that T is standard notation for a torus in this game but your T is not :-)

[Alex Brodbelt]

What should I rename it to?

[Kevin Buzzard]

It's usually called N isn't it?

[Alex Brodbelt]

Kevin Buzzard said:

One problem with this thread is that it just launches into a wall of maths without giving any definitions. This just leads to confusion. Alex can you tell us what F is? It would be nice if the question was self-contained rather than just assuming everyone has remembered you're previous questions

Is it easier if I make a new thread and begin giving out context to where I am at and where I am heading or should I just do that here?

[Kevin Buzzard]

Why not just edit the top post so that the question actually becomes readable? Another question: what is p? The first time you mention it is "every element has order p". Is it prime?

[Alex Brodbelt]

It is the characteristic of the field, so yes it is prime.

[Kevin Buzzard]

So F is not any algebraically closed field? It must have finite characteristic? Or can p be 0?

[Alex Brodbelt]

I am going through all cases when $p= 0$, $p = 2$ and when $p$ is a prime not equal to $2$

[Alex Brodbelt]

for this particular case I am considering when $p \neq 0$

[Alex Brodbelt]

I eventually would like to cover the case $p = 0$ but that will be a bit later

[Kevin Buzzard]

So what does "every element has order p" mean? What about the identity element? Can p be 1?

It would not take much effort on your part to ask a question which was (a) self-contained and (b) accurate. I am quite autistic and slips really throw me. I didn't even read your question because I was lost after the first line (and because I was running Lean Together so didn't have time to reconstruct what you meant from what you wrote). But now someone else has attempted to, I think it might be better if I push you to actually make the question comprehensible.

[Kevin Buzzard]

Alex Brodbelt said:

for this particular case I am considering when $p \neq 0$

Then say that in the question? People can't guess hypotheses which you don't write down. I'm trying to encourage you to ask better questions.

[Alex Brodbelt]

Ok I'll write all the details down :)

[Kevin Buzzard]

Thanks :-)

[to anyone else reading: the context here is that Alex is a student working on a project I've given him]

[Alex Brodbelt]

Artie Khovanov said:

I'm a bit confused about what you're assuming and what you're trying to prove, but I'll try my best. Since $Z$ commutes with everything, we have

$A=(c^{-1}TZc)\cap G=(c^{-1}Tc\cdot Z)\cap G=(c^{-1}Tc\cap G)Z.$

So it's enough to show that $c^{-1}Tc\cap G\cong T\cap cGc^{-1}$ is elementary abelian.

Now, I think you've told me you can prove that $T_0=T\cap G$ is elementary abelian. If you do this proof with $G$ replaced by $cGc^{-1}$, which is also a subgroup containing the centre, then you're done.

Sorry if I made a wrong assumption somewhere!

I am trying to define the isomorphism but I am not sure how to remove the use of tactics (I am aware using tactics when defining functions is nono):

How can one detactify this? I can convert simple proofs to their corresponding proof terms but not so sure about this one:

def conj_T_meet_G_iso_T_meet_conj_inv_G {F : Type*} [Field F] (c : SL(2,F)) (G : Subgroup SL(2,F)) (hG : center SL(2,F) ≤ G) :
  (conj c • T F ⊓ G:) ≃* (T F ⊓ conj c⁻¹ • G:) where
  toFun :=
    fun ⟨x, x_in_conj, x_in_G⟩ =>
      ⟨c⁻¹ * x * c,
      by
      rw [mem_inf]
      obtain ⟨t, ht, h⟩ := x_in_conj
      simp at h
      constructor
      · rw [← h]
        group
        exact ht
      · simp [pointwise_smul_def]
        exact x_in_G
      ⟩
  invFun :=
    fun ⟨t, ht, t_in_conj⟩ =>
      ⟨c * t * c⁻¹,
      by
      rw [mem_inf]
      obtain ⟨g, g_in_G, h⟩ := t_in_conj
      simp at h
      constructor
      · simp [pointwise_smul_def]
        exact ht
      · rw [← h]
        group
        exact g_in_G
      ⟩
  left_inv := sorry
  right_inv := sorry
  map_mul' := sorry

[Andrew Yang]

It's fine if the goal of the tactis is a prop (which seems to be the case here?).

[Alex Brodbelt]

At the left_inv sorry this is what the infoview looks like:

left_inv_sorry

It does not look very amenable :-(

[Alex Brodbelt]

Ah wait nvm

[Artie Khovanov]

Alex Brodbelt said:

Artie Khovanov said:

I am trying to define the isomorphism but I am not sure how to remove the use of tactics (I am aware using tactics when defining functions is nono):

I think you misunderstand. Using tactic mode can be problematic when constructing data, not proofs. This is because the inner workings of a proof get erased by Lean (if you want to know more, look up "proof irrelevance axiom"). It doesn't matter to Lean how you close a goal of type Prop.

By the way, thanks for writing your assumptions up, and providing a reference. The proof bit (second part) is still quite unclear, though. I think this is because you are not clear on what you've already proved informally, what you've already proved in Lean, and what you think/know is true, but do not know how to prove.

You also don't define $c$ or the $\tau$ you're using anywhere. Do we have $\tau\neq0$? What about $t_\tau\in G$? Can it be any $\tau$ satisfying certain conditions, or are you saying only that some such $\tau$ exists? I know these questions must sound silly or trivial given all the knowledge and context that you have, but you should keep in mind that someone seeing all this for the first time (i.e., your intended audience) will not be able to guess these things without putting in work, which makes what you write much harder to parse. The easiest way to make sure your work is readable is to present as complete and self-contained a mathematical argument as possible, noting what you have formalised and where you are unclear.

I managed to figure out roughly what you meant in the end based on context, but you should know that it took me over an hour!

[Artie Khovanov]

Kevin Buzzard said:

It would not take much effort on your part to ask a question which was (a) self-contained and (b) accurate. I am quite autistic and slips really throw me.

Yeah I mean I got confused and just tried doing the problem myself. Then I guessed what assumptions must be present from that.

[Kevin Buzzard]

Alex Brodbelt said:

Ok I'll write all the details down :)

Alex thanks so much for making the question comprehensive and readable! Just to reiterate what Andrew said -- tactic mode is fine if your goal is ⊢ P with P : Prop and is possibly not fine if your goal is ⊢ T with T : Type u.

[Kevin Buzzard]

I still find it slightly grating that your definition of $A$ mentions $G$ but you don't define $G$ until later.

Your claim that $C_{SL(2,F)}(t_\tau)=T\cup Z(SL(2,F))$ is incorrect if $\tau=0$ (and this can happen if e.g. $G$ is abelian). Can you clarify whether you are interested in this case?

You have $A$ a subgroup of $G$, and then you say $A\cong C_G(t_\tau)$. But $C_G(t_\tau)$ and $A$ are both subgroups of $G$. Do you mean $A=C_G(t_\tau)$ or not? Equality of groups is in general a meaningless concept in Lean. But equality of subgroups is very much meaningful.

[Alex Brodbelt]

I will update the current state of where I am and the original question, so it is more pertinent to the current state (and more pertinent in general), one second. I apologise for the gaps in information and the wasted time (sorry, I had lectures all day...).

[Alex Brodbelt]

OK... I think those are most if not all details

[Alex Brodbelt]

For the isomorphism I need outlined at the top of this thread:

This part I figured out in the end:

def conj_T_meet_G_eq_T_conj_G {F : Type*} [Field F] (c : SL(2,F)) (G : Subgroup SL(2,F)) (hG : center SL(2,F) ≤ G) :
  (conj c • T F ⊓ G:) ≃* (T F ⊓ conj c⁻¹ • G:) where
  toFun :=
    fun x =>
      ⟨c⁻¹ * x * c,
      by
      obtain ⟨x_in_conj, x_in_G⟩ := x.property
      rw [mem_inf]
      obtain ⟨t, ht, h⟩ := x_in_conj
      simp at h
      constructor
      · rw [← h]
        group
        exact ht
      · simp [pointwise_smul_def]
        exact x_in_G
      ⟩
  invFun :=
    fun t =>
      ⟨c * t * c⁻¹,
      by
      obtain ⟨t_in_T, t_in_conj⟩ := t.property
      rw [mem_inf]
      obtain ⟨g, g_in_G, h⟩ := t_in_conj
      simp at h
      constructor
      · simp [pointwise_smul_def]
        exact t_in_T
      · rw [← h]
        group
        exact g_in_G
      ⟩
  left_inv := by
    simp [LeftInverse]
    rintro x ⟨t, t_in_T, h⟩ x_in_G
    group
  right_inv := by
    simp [Function.RightInverse, LeftInverse]
    rintro t t_in_T ⟨g, g_in_G, h⟩
    group
  map_mul' := by
    rintro ⟨x₁, ⟨t₁, t₁_in_T, rfl⟩, x₁_in_G⟩ ⟨x₂, ⟨t₂, t₂_in_T, rfl⟩, x₂_in_G⟩
    simp
    group

The part I am not able to piece yet but should be easyish but then can follow MIL to get the desired isomorphism. I am a bit clumsy with quotients in Lean :(

import Mathlib

open Subgroup

lemma card_mul_normal {G : Type*} [Group G] (H N : Subgroup G) [hH : Finite H] [hN : Finite N] [hN' : N.Normal] : Nat.card (H ⊔ N :) = Nat.card H * Nat.card N := by
  have : Nat.card (H ⊔ N :) = Nat.card ((H ⊔ N :) : Set G) := by simp only [SetLike.coe_sort_coe]
  rw [this, Subgroup.mul_normal]
  rw [@card_mul_eq_card_subgroup_mul_card_quotient]
  let f : ↥H →* G ⧸ N := (QuotientGroup.mk' N).restrict H
  have : Nat.card ((@QuotientGroup.mk G _ N '' (H : Set G))) = Nat.card H := by
    -- would like to use f
    refine Eq.symm (Nat.card_eq_of_bijective ?f ?hf)
    sorry
    sorry
  sorry

[Artie Khovanov]

Your second theorem is untrue. For instance, what if $H=N$? You need an additional assumption.

[Artie Khovanov]

Alex Brodbelt said:

The last isomorphism is constructed by feeding in one isomorphism into another:
From the isomorphism $c^{−1}Tc\sqcap G\cong T\sqcap cGc^{−1}$ and $A \sqcup Z = B \sqcup Z$ for $A \cong B$, $Z$ normal (as commutative) and trivial intersection between $Z \sqcap A = \{1\} = Z \sqcap B$. this is what I am stuck trying to formalize

It's easier than this. You can apply the conjugation by $c$ to the whole subgroup, and get your isomorphism in one step! You just need to prove that the conjugation action (or really any group isomorphism) preserves certain operations on subgroups.

[Alex Brodbelt]

Ah I forgot to add disjointness

[Alex Brodbelt]

Hmm so something like "simplifying" (might not be quite right but the idea you mean is something along these line):

$c c^{-1} T c \sqcap G \sqcup Z c^{-1}$

[Artie Khovanov]

Alex Brodbelt said:

Hmm so something like "simplifying":

$c c^{-1} T c \sqcap G \sqcup Z c^{-1}$

You could do this, and it will work out, but I think a more conceptual approach works better here, and is less messy.

What you're really saying is that these two subgroups are conjugate by $c$, and the conjugation action of $c$ is just an automorphism of $G$. So it preserves product and intersection of subgroups.

[Artie Khovanov]

Then all you need to check is what happens when you conjugate each of c^-1Tc, G, Z by c
That requires computations, of course, but they are easier

[Artie Khovanov]

How much API about the conjugation action is there in Mathlib already, I wonder

[Artie Khovanov]

Yeah OK eg Subgroup.map_inf_eq, ConjAct.fixedPoints_eq_center etc are your friends here
LeanSearch is very helpful for finding results like these!

[Alex Brodbelt]

Hmm yes

[Alex Brodbelt]

I desperately need sleep :zzz:, brain is not thinking right now. Thanks Artie

[Alex Brodbelt]

Cool! has been done, now moving on to proving properties of $Q$

[Alex Brodbelt]

I have finished Lemma 2.3.iii in the exposition I provided above, took a bit more effort than I thought. Thanks for the help :)

[Alex Brodbelt]

I was a bit surprised some lemmas I needed were not in mathlib such an example would be:

lemma ne_zero_two_of_char_ne_two {p : ℕ} [hp' : Fact (Nat.Prime p)]
  [hC : CharP F p] (p_ne_two : p ≠ 2) : NeZero (2 : F) := by
  refine { out := ?_ }
  intro two_eq_zero
  have one_ne_zero : (1 : F) ≠ 0 := one_ne_zero
  let char_eq_two : CharP F 2 := by
    exact CharTwo.of_one_ne_zero_of_two_eq_zero one_ne_zero two_eq_zero
  have two_dvd_p : (p : F) = 0 := by exact CharP.cast_eq_zero F p
  rw [char_eq_two.cast_eq_zero_iff'] at two_dvd_p
  have two_eq_p : p = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hp'.out).mp two_dvd_p).symm
  contradiction

[Artie Khovanov]

What about NeZero.of_not_dvd?

[Alex Brodbelt]

Aha, strange apply? or leansearch did not suggest this...

[Artie Khovanov]

apply? isn't very helpful in this situation

[Artie Khovanov]

but you still need to do a little work, of course
because you need to show characteristic isn't 1
but you're in a field so you're good

[Artie Khovanov]

if you wanted to do this for any prime (not just 2), there's CharP.char_is_prime, and I'm sure there's a lemma that says "prime p divides prime q iff p=q"

[Alex Brodbelt]

That lemma would be Nat.prime_dvd_prime_iff_eq

[Alex Brodbelt]

Cheers!

[Alex Brodbelt]

I am trying to define an isomorphism from $PSL_n(F)$ to $PGL_n(F)$ when $F$ is algebraically closed (having stopped to think about it, I believe characteristic is irrelevant - we will see what lean says though), informally this is my proof:

Let $\varphi : \textrm{PSL}_n(F) \rightarrow \textrm{PGL}_n(F)$ be defined by
$S \; \langle \omega I\rangle \mapsto i(S) \; (F^\times I)$

where $i : \textrm{SL}_n(F) \hookrightarrow \textrm{GL}_n(F)$ is the natural injection of the special linear group into the general linear group.

We show $\varphi$ is an isomorphism when $F$ is algebraically closed

• We show $\varphi$ is well-defined:

Let $S, S' \in \textrm{SL}_n(F)$, suppose $S \langle \omega I\rangle = S'\langle \omega I\rangle$ then because $SS'^{-1} \in \langle -I\rangle \iff SS'^{-1} = \omega^k I$ for some $k \in \mathbb{N}$ we have the following chain of set equalities

$\varphi(S \langle \omega I \rangle) = S (F^\times I) = S' (F^\times I) = \varphi(S' \langle \omega I\rangle)$

because $S = \omega^k I S$ and $\omega I \in F^\times I$

• When $F$ is algebraically closed, we show $\varphi$ in fact defines an isomorphism:

We show $\varphi$ is multiplicative, injective and surjective (low-tech way):

• $\varphi$ is multiplicative:

  Let $S \langle-I\rangle, Q\langle-I\rangle \in \textrm{PSL}_n(F)$ where $S, Q \in \textrm{SL}_n(F)$ then

$$\begin{align*} \varphi(S \langle-I\rangle Q\langle-I\rangle ) &= \varphi(SQ \langle -I\rangle)\\ &= i(SQ) F^\times I\\ &= i(S) i(Q) F^\times I\\ &= i(S) (F^\times I) \cdot i(Q)(F^\times I) \\ &= \varphi(S) \varphi(Q) \end{align*}$$

Where the normality of $\langle \omega I \rangle$ is used, and because group injections define a homomorphism and by the normality of $F^\times I$.

• $\varphi$ is injective:

Let $S \langle -I\rangle, S'\langle-I\rangle \in \textrm{PSL}_n(F)$ and suppose
$\varphi(S \langle -I\rangle) = \varphi(S'\langle-I\rangle)$ then $i(S) (F^\times I) = i(S')(F^\times I)$ further implies $i(S) i(S')^{-1} = cI$

but $i(S) i(S')^{-1} = i(S S'^{-1})$ so $\det(i(S)i(S')^{-1}) = c^n = 1$ and thus
$c = \omega^k$ for some $k \in \N$, where $\omega$ is a primitive $$n$$th root of unity.

$$\begin{align*} \varphi(S \langle-I\rangle Q\langle-I\rangle ) &= \varphi(SQ \langle -I\rangle) \\ &= i(SQ) F^\times I\\ &= i(S) i(Q) F^\times I\\ &= i(S) (F^\times I) \cdot i(Q)(F^\times I) \\ &= \varphi(S) \varphi(Q) \end{align*}$$

• $\varphi$ is surjective:

Let $G \; (F^\times I) = [G] \in \textrm{PGL}_n(F)$, then $G \in \textrm{GL}_n(F)$ and so $\det G \ne 0$, we can find a representative of $[G']$, that lies within the special linear group.Given elements of the special linear group are matrices with determinant equal to one, we must scale $G$ to a suitable factor to yield a representative which lies within $\textrm{SL}_n(F)$. Let

$P(X) := X^n - \det(G) \in F[X]$

By assumption, $F$ is algebraically closed so there exists a root $\alpha \ne 0\in F$ such that

$\alpha^n - \det(G) = 0 \iff \alpha^n = \det(G)$

We can define

$G' := \frac{1}{\alpha} \cdot G$ where $\det(G') = \frac{1}{\alpha^n} \det(G) = 1$
Thus $G' \in \textrm{SL}_n(F) \leq \textrm{GL}_n(F)$ and given $G' = \frac{1}{\alpha} G$ we have that
$G' \; (F^\times I) = G \; (F^\times I)$.

Therefore, $\varphi(G') = i(G') (F^\times I) = G' (F^\times I) = G (F^\times I)$.

So far I am definining the monoid homomorphism from $PSL_n(R)$ into $PGL_n(R)$ when $R$ is a commutative ring with some more assumptions on the ring.

But I am poor with using the quotient type, so I am not sure how to define the map in the first place, so far I have this

import Mathlib

open Subgroup MatrixGroups Matrix LinearMap

noncomputable def MonoidHom_PSL_into_PGL {R : Type*} [CommRing R] {n : ℕ} :
  SpecialLinearGroup (Fin n) R ⧸ center (SpecialLinearGroup (Fin n) R) →* GL (Fin n) R ⧸ center (GL (Fin n) R) where
  toFun S := by
    let G := QuotientGroup.mk' (center (GL (Fin n) R)) S.exists_rep.choose.toGL
    use G
    -- I would like to do this without tactics
  map_one' := sorry
  map_mul' := sorry

not that computability matters anyway, but I presume it doesn't necessarily have to be noncomputable?

[Kevin Buzzard]

You should be using (n : Type*) [Fintype n] rather than Fin n, the proof will be no harder and your result will be more general. You definitely should not be using the axiom of choice to define this map though! Use QuotientGroup.map and it will all be easy.

[Artie Khovanov]

What you're trying to do, mathematically, is "lift" a homomorphism f:R->S to a quotient R/I->S. You can do this exactly when f(I)={0}. This also gives you multiplicativity for free! As Kevin says, Lean already has a way to do this.

[Artie Khovanov]

Also when you're showing injectivity you can just show the kernel is trivial, that's easier than your thing.

[Kevin Buzzard]

Your informal proof is not really valid in Lean because it makes the assumption (which you were probably taught, so this is not your fault) that an element of a quotient group is equal to a coset. This is not true in Lean; to work with quotient groups you should use universal properties like QuotientGroup.lift and QuotientGroup.map; the axiom needed to apply these functions is precisely what you were told was the check that your functions from the quotient were "well-defined".

[Artie Khovanov]

@Kevin Buzzard the whole coset vs quotient type thing to me feels like a distinction often made wrt Lean without a difference; surely you work with both in exactly the same way?

[Alex Brodbelt]

Ok it seems I have something to chew on

[Alex Brodbelt]

Is there any other reference for quotient type other than the Lean Reference Manual?

[Artie Khovanov]

Lean implements its quotients in a fairly unique way as I understand

[Artie Khovanov]

There's this quick overview: https://leanprover-community.github.io/mathematics_in_lean/C09_Linear_Algebra.html#subspaces-and-quotients

[Kevin Buzzard]

I'm just writing a blog post now. Artie I don't agree that you work with both in exactly the same way: when showing phi is well-defined above, Alex is specifically working with cosets. Look at his definition of a map from a quotient: choose a random representative using the axiom of choice and define the function on the representative. That is exactly what students are being told to do in maths departments and it is not at all what you do in Lean.

[Artie Khovanov]

I guess I am already thinking about quotients abstractly

[Alex Brodbelt]

I have successfully used QuotientGroup.lift to produce a monoid homomorphism from PSL n R →* PGL n R (see PSL_monoidHom_PGL).

Now trying to generate the monoid homomorphism in the other direction, I was thinking of first defining
GL n F →* SL n F (*) and then using the canonical homomorphism SL n R →* PSL n R (specialized for F - see SL_monoidHom_PSL).

It is (*) that I am having trouble with as I need to use algebraic closure to extract an nth root of $\det G$ where $G \in \textrm{GL}_n(F)$.

I have the lemma for extracting this nth root and the corresponding matrix in $\textrm{SL}_n(F)$ but I am not sure how to use it for contructing the monoid homomorphism, so far I can construct the data using tactics and choice, but then as expected the proofs become intractable (see GL_monoidHom_SL).

A reasonable chunk of this code is for proving properties about the center of $\textrm{GL}_n(R)$, so you can ignore a lot of it, i.e: skip to the bottom for the relevant code.

import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs


universe u v w

open Matrix

open scoped MatrixGroups

variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (F : Type w) [Field F]


scoped[MatrixGroups] notation "SL"  => Matrix.SpecialLinearGroup

def Matrix.transvection.toSL {i j : n} (hij : i ≠ j) (c : R): SL n R :=
  ⟨Matrix.transvection i j c, (det_transvection_of_ne i j hij (c : R))⟩


namespace Matrix.TransvectionStruct

open Matrix

def toSL (t : TransvectionStruct n R) : SL n R := Matrix.transvection.toSL t.hij t.c

def toGL (t : TransvectionStruct n R) : GL n R := Matrix.transvection.toSL t.hij t.c

end Matrix.TransvectionStruct

namespace GeneralLinearGroup

def scalar (n : Type*) [DecidableEq n] [Fintype n] (r : Rˣ) : GL n R :=
  Units.map (Matrix.scalar n).toMonoidHom r

/-- scalar matrix belongs to GL n R iff r is a unit -/
theorem coe_scalar_matrix (r : Rˣ) : Matrix.scalar n r.val = scalar n r := rfl

/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). -/
theorem mem_range_scalar_of_commute_transvectionStruct' {M : GL n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toGL M):
    (M : Matrix n n R) ∈ Set.range (Matrix.scalar n) := by
  refine mem_range_scalar_of_commute_transvectionStruct ?_
  simp_rw [← Commute.units_val_iff] at hM
  exact hM

theorem mem_range_unit_scalar_of_mem_range_scalar_and_mem_general_linear_group {M : GL n R} (hM : (M : Matrix n n R) ∈ Set.range (Matrix.scalar n)) :
    ∃ r : Rˣ, scalar n r = M := by
    obtain ⟨r', hr'⟩ := hM
    have det_scalar : (Matrix.scalar n r').det = r'^(Nat.card n) := by simp
    have det_M_is_unit: IsUnit ((M : Matrix n n R).det) := by simp only [isUnits_det_units]
    rw [← hr', det_scalar] at det_M_is_unit
    by_cases hn : Nat.card n ≠ 0
    · have r'_is_unit : IsUnit r' := by rw [← isUnit_pow_iff hn]; exact det_M_is_unit
      obtain ⟨r, hr⟩ := r'_is_unit
      use r
      have h : scalar n r = Matrix.scalar n r' := by simp [scalar]; intro _n; exact hr
      ext
      rw [h, hr']
    · simp only [Nat.card_eq_fintype_card, ne_eq, Decidable.not_not] at hn
      use 1
      rw [scalar]; simp only [RingHom.toMonoidHom_eq_coe, _root_.map_one]
      ext
      have n_empty : IsEmpty n := by rw [← Fintype.card_eq_zero_iff, hn]
      rw [← units_eq_one M]


theorem mem_units_range_scalar_iff_commute_transvectionStruct {R : Type v} [CommRing R] (M : GL n R) : (∀ (A : GL n R), Commute A M) ↔ (∃ r : Rˣ, scalar n r = M) := by
  constructor
  · intro hM
    -- if M commutes with every matrix then it must commute with the transvection matrices
    have h₀ : ∀ (t : TransvectionStruct n R), Commute (t.toGL) M := fun t => hM t.toGL
    -- if M commutes with the transvection matrices then M ∈ Set.range (Matrix.scalar n) where Set.range is Rˣ
    have h₁ : (M : Matrix n n R) ∈ Set.range ⇑(Matrix.scalar n) := mem_range_scalar_of_commute_transvectionStruct' h₀
    have h₂ : ∃ r : Rˣ, scalar n r = M := mem_range_unit_scalar_of_mem_range_scalar_and_mem_general_linear_group h₁
    obtain ⟨r, rfl⟩ := h₂
    use r
  · intro h A
    obtain ⟨r, rfl⟩ := h
    ext i j
    rw [
      GeneralLinearGroup.coe_mul, GeneralLinearGroup.coe_mul,
      ← coe_scalar_matrix, scalar_commute
      ]
    exact fun r' ↦ Commute.all (↑r) r'

namespace Center

open Subgroup GeneralLinearGroup

theorem mem_center_general_linear_group_iff {M : GL n R} : M ∈ Subgroup.center (GL n R) ↔ (∃ r : Rˣ, scalar n r = M) := by
  rw [mem_center_iff]
  constructor
  · intro h
    rw [← mem_units_range_scalar_iff_commute_transvectionStruct]
    congr
  · intro h A
    have hA : (∀ (A : GL n R), Commute A M) :=
      (mem_units_range_scalar_iff_commute_transvectionStruct M).mpr h
    exact Commute.eq <| hA A

end Center

end GeneralLinearGroup

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

open Subgroup

/-- A projective general linear group is the quotient of a special linear group by its center. -/
abbrev ProjectiveGeneralLinearGroup : Type _ :=
    GL n R ⧸ center (GL n R)


/-- `PGL n R` is the projective special linear group `(GL n R)/ Z(GL(n R))`. -/
abbrev PGL := ProjectiveGeneralLinearGroup


open Matrix LinearMap Subgroup

open scoped MatrixGroups


variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

/-- A projective special linear group is the quotient of a special linear group by its center. -/
abbrev ProjectiveSpecialLinearGroup : Type _ :=
    SpecialLinearGroup n R ⧸ center (SpecialLinearGroup n R)

/-- `PSL(n, R)` is the projective special linear group `SL(n, R)/Z(SL(n, R))`. -/
abbrev PSL := ProjectiveSpecialLinearGroup


namespace Isomorphism

variable (n : ℕ) (F : Type u) [Field F] [IsAlgClosed F]

open Subgroup

def SL_monoidHom_PGL (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] :
  SL n R →*  PGL n R where
  toFun S := QuotientGroup.mk' (center (GeneralLinearGroup n R)) S.toGL
  map_mul' S₁ S₂ := by simp
  map_one' := by simp

lemma coe  {n : Type*}  [Fintype n] [DecidableEq n] (x : SpecialLinearGroup n R): SpecialLinearGroup.toGL x = (x : Matrix n n R) := rfl

lemma center_SL_le_ker (n : Type*) [Nonempty n] [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] [NeZero (1 : R)]: center (SpecialLinearGroup n R) ≤ (SL_monoidHom_PGL n R).ker := by
  intro x x_mem_center
  rw [SpecialLinearGroup.mem_center_iff] at x_mem_center
  obtain ⟨ω, hω, h⟩ := x_mem_center
  simp [MonoidHom.mem_ker, SL_monoidHom_PGL]
  rw [GeneralLinearGroup.Center.mem_center_general_linear_group_iff]
  have IsUnit_ω : IsUnit ω := IsUnit.of_pow_eq_one hω Fintype.card_ne_zero
  use IsUnit_ω.unit
  ext
  simp [← GeneralLinearGroup.coe_scalar_matrix, coe, ← h]

instance center_is_normal (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n] [CommRing R] [NeZero (1 : R)] : Subgroup.Normal (center (SpecialLinearGroup n R)) := normal_of_characteristic (center (SL n R))

instance PGL_is_monoid  (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n] [CommRing R] [NeZero (1 : R)] : Monoid (ProjectiveGeneralLinearGroup n R) := RightCancelMonoid.toMonoid

def PSL_monoidHom_PGL (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n] [CommRing R] [NeZero (1 : R)] :
  PSL n R →* PGL n R :=
  @QuotientGroup.lift (SL n R) _ (center (SL n R)) (center_is_normal n R) (PGL n R) (PGL_is_monoid n R) (SL_monoidHom_PGL n R) (center_SL_le_ker n R)

open Polynomial


lemma exists_SL_eq_scaled_GL_of_IsAlgClosed {n F : Type*} [hn₁ : Fintype n] [DecidableEq n] [hn₂ : Nonempty n] [Field F] [IsAlgClosed F] (G : GL n F) : ∃ c : Fˣ, ∃ S : SL n F,  c • S.toGL = G := by
  let P : F[X] := X^(Nat.card n) - C (det G.val)
  have nat_card_ne_zero : (Nat.card n) ≠ 0 := Nat.card_ne_zero.mpr ⟨hn₂, Fintype.finite hn₁⟩
  have deg_P_ne_zero : degree P ≠ 0 := by
    rw [Polynomial.degree_X_pow_sub_C]
    exact Nat.cast_ne_zero.mpr nat_card_ne_zero
    exact Nat.card_pos
  obtain ⟨c, hc⟩ := @IsAlgClosed.exists_root F _ _ P deg_P_ne_zero
  have c_ne_zero : c ≠ 0 := by
    rintro rfl
    simp [P] at hc
    have det_G_ne_zero : det G.val ≠ 0 := IsUnit.ne_zero <| isUnits_det_units G
    contradiction
  have IsUnit_c : IsUnit c := by exact Ne.isUnit c_ne_zero
  have hc' : ∃ c : Fˣ, c^(Nat.card n) = det G.val := by
    use IsUnit_c.unit
    simp [P, sub_eq_zero] at hc
    simp [hc]
  obtain ⟨c, hc⟩ := hc'
  have det_inv_c_G_eq_one : det (c⁻¹ • G).1 = (1 : F) := by
    simp [← hc, inv_smul_eq_iff, Units.smul_def]
  use c, ⟨(c⁻¹ • G), det_inv_c_G_eq_one⟩
  ext
  simp [coe]

noncomputable def GL_monoidHom_SL (n F : Type*) [Fintype n] [DecidableEq n] [Nonempty n] [Field F] [IsAlgClosed F] :
  GL n F →* SL n F where
  toFun G := by
    obtain c := (exists_SL_eq_scaled_GL_of_IsAlgClosed G).choose
    obtain S := (exists_SL_eq_scaled_GL_of_IsAlgClosed G).choose_spec.choose
    obtain h := (exists_SL_eq_scaled_GL_of_IsAlgClosed G).choose_spec.choose_spec
    use S
    exact SpecialLinearGroup.det_coe S
  map_mul' G₁ G₂ := by
    simp
    sorry
  map_one' := by
    simp
    sorry

def SL_monoidHom_PSL (n R : Type*) [Fintype n] [DecidableEq n] [Nonempty n] [CommRing R] :
  SL n R →* PSL n R := QuotientGroup.mk' (center (SL n R))


def GL_monoidHom_PSL (n F : Type*) [Fintype n] [DecidableEq n] [Nonempty n] [Field F] [IsAlgClosed F]  :
  GeneralLinearGroup n F →* ProjectiveSpecialLinearGroup n F := sorry--SL_monoidHom_PSL.comp GL_monoidHom_SL


-- We define the isomorphism between the projective general linear group and the projective special linear group
def PGL_iso_PSL (n F : Type*) [Fintype n] [DecidableEq n] [Nonempty n] [Field F] [IsAlgClosed F] : ProjectiveGeneralLinearGroup n F ≃* ProjectiveSpecialLinearGroup n F where
  toFun := sorry
  invFun := PSL_monoidHom_PGL n F
  left_inv := sorry
  right_inv := sorry
  map_mul' := sorry

end Isomorphism

[Artie Khovanov]

I wouldn't define an inverse here; I would just prove my map was bijective. Like, your inverse isn't computable anyway.

[Alex Brodbelt]

So you would use docs#MulEquiv.ofBijective ?

[Artie Khovanov]

That sounds right.

[Alex Brodbelt]

I was thinking of this too, but the typeclasses involved put me off it and opted for this.

I did not stop to think if the inverse was compatible though, I assumed it would be.

[Alex Brodbelt]

Btw this would be great for tomorrow's lean club if I get it done in time!

[Artie Khovanov]

The reason computability "matters" is that doing it using ofBijective means that your inverse isn't computable -- you need to use Lean's "axiom of choice" to obtain it. So if your inverse is computable it's slightly better to give it explicitly (at the cost of having to do a bit more work). However, as you yourself say above, you need to extract an nth root using choice, so you don't even get this advantage!

[Alex Brodbelt]

So trying to prove bijectivity of PSL_monoidHom_PGL to then use MulEquiv.ofBijective but I am stuck whenever I have a term of type PSL n F or PGL n F.

I'd like to extract a representative or some equivalent thing so I have a term of type SL n For GL n F and then use the lemmas I have to show that in fact be a root of unity and so forth, and so the lift of this element equals the term of type PSL n For PGL n F respectively.

Again, a lot of the code is "boilerplate" theorems and definitions, so skip to the bottom to see the lemma I am struggling with:

import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

set_option linter.style.longLine true
set_option autoImplicit false
set_option maxHeartbeats 0

universe u v w

open Matrix

open scoped MatrixGroups

variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (F : Type w) [Field F]


scoped[MatrixGroups] notation "SL"  => Matrix.SpecialLinearGroup

def Matrix.transvection.toSL {i j : n} (hij : i ≠ j) (c : R): SL n R :=
  ⟨Matrix.transvection i j c, (det_transvection_of_ne i j hij (c : R))⟩


namespace Matrix.TransvectionStruct

open Matrix

def toSL (t : TransvectionStruct n R) : SL n R := Matrix.transvection.toSL t.hij t.c

def toGL (t : TransvectionStruct n R) : GL n R := Matrix.transvection.toSL t.hij t.c

end Matrix.TransvectionStruct

namespace GeneralLinearGroup

def scalar (n : Type*) [DecidableEq n] [Fintype n] (r : Rˣ) : GL n R :=
  Units.map (Matrix.scalar n).toMonoidHom r

/-- scalar matrix belongs to GL n R iff r is a unit -/
theorem coe_scalar_matrix (r : Rˣ) : Matrix.scalar n r.val = scalar n r := rfl

/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). -/
theorem mem_range_scalar_of_commute_transvectionStruct' {M : GL n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toGL M):
    (M : Matrix n n R) ∈ Set.range (Matrix.scalar n) := by sorry --ommited

theorem mem_range_unit_scalar_of_mem_range_scalar_and_mem_general_linear_group {M : GL n R}
  (hM : (M : Matrix n n R) ∈ Set.range (Matrix.scalar n)) :
    ∃ r : Rˣ, scalar n r = M := by sorry --ommited


theorem mem_units_range_scalar_iff_commute_transvectionStruct {R : Type v} [CommRing R]
  (M : GL n R) : (∀ (A : GL n R), Commute A M) ↔ (∃ r : Rˣ, scalar n r = M) := by sorry --ommited

namespace Center

open Subgroup GeneralLinearGroup

theorem mem_center_general_linear_group_iff {M : GL n R} :
  M ∈ Subgroup.center (GL n R) ↔ (∃ r : Rˣ, scalar n r = M) := by sorry --ommited

end Center

end GeneralLinearGroup

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

open Subgroup

/-- A projective general linear group is the quotient of a special linear group by its center. -/
abbrev ProjectiveGeneralLinearGroup : Type _ :=
    GL n R ⧸ center (GL n R)


/-- `PGL n R` is the projective special linear group `(GL n R)/ Z(GL(n R))`. -/
abbrev PGL := ProjectiveGeneralLinearGroup


open Matrix LinearMap Subgroup

open scoped MatrixGroups


variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

/-- A projective special linear group is the quotient of a special linear group by its center. -/
abbrev ProjectiveSpecialLinearGroup : Type _ :=
    SpecialLinearGroup n R ⧸ center (SpecialLinearGroup n R)

/-- `PSL(n, R)` is the projective special linear group `SL(n, R)/Z(SL(n, R))`. -/
abbrev PSL := ProjectiveSpecialLinearGroup


namespace Isomorphism

variable (n : ℕ) (F : Type u) [Field F] [IsAlgClosed F]

open Subgroup

def SL_monoidHom_GL  (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] :
  SL n R →* GL n R := SpecialLinearGroup.toGL

def GL_monoidHom_PGL (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] :
  GL n R →* PGL n R := QuotientGroup.mk' (center (GL n R))

def SL_monoidHom_PGL (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] :
  SL n R →*  PGL n R :=  MonoidHom.comp (GL_monoidHom_PGL n R) (SL_monoidHom_GL n R)

lemma coe  {n : Type*}  [Fintype n] [DecidableEq n] (x : SpecialLinearGroup n R):
  SpecialLinearGroup.toGL x = (x : Matrix n n R) := rfl

lemma center_SL_le_ker (n : Type*) [Nonempty n] [Fintype n] [DecidableEq n]
  (R : Type*) [CommRing R] [NeZero (1 : R)]:
  center (SpecialLinearGroup n R) ≤ (SL_monoidHom_PGL n R).ker := by sorry --ommited

instance center_is_normal (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n]
  [CommRing R] [NeZero (1 : R)] : Subgroup.Normal (center (SpecialLinearGroup n R)) :=
  normal_of_characteristic (center (SL n R))

instance PGL_is_monoid  (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n]
  [CommRing R] [NeZero (1 : R)] : Monoid (ProjectiveGeneralLinearGroup n R) :=
  RightCancelMonoid.toMonoid

def PSL_monoidHom_PGL (n R : Type*) [Nonempty n] [Fintype n] [DecidableEq n]
  [CommRing R] [NeZero (1 : R)] :
  PSL n R →* PGL n R :=
  @QuotientGroup.lift (SL n R) _ (center (SL n R)) (center_is_normal n R) (PGL n R)
    (PGL_is_monoid n R) (SL_monoidHom_PGL n R) (center_SL_le_ker n R)

open Polynomial


lemma exists_SL_eq_scaled_GL_of_IsAlgClosed {n F : Type*} [hn₁ : Fintype n] [DecidableEq n]
  [hn₂ : Nonempty n] [Field F] [IsAlgClosed F] (G : GL n F) :
  ∃ c : Fˣ, ∃ S : SL n F,  c • S.toGL = G := by
  let P : F[X] := X^(Nat.card n) - C (det G.val)
  have nat_card_ne_zero : (Nat.card n) ≠ 0 := Nat.card_ne_zero.mpr ⟨hn₂, Fintype.finite hn₁⟩
  have deg_P_ne_zero : degree P ≠ 0 := by sorry --ommited

open Function


lemma lift_scalar_matrix_eq_one {n F : Type*} [hn₁ : Fintype n] [DecidableEq n]
  [Field F] [IsAlgClosed F] (c : Fˣ) : GL_monoidHom_PGL n F (c • 1)  = 1 := by sorry --ommited


lemma Bijective_PSL_monoidHom_PGL {n F : Type*} [hn₁ : Fintype n] [DecidableEq n]
  [hn₂ : Nonempty n] [Field F] [IsAlgClosed F] :  Bijective (PSL_monoidHom_PGL n F) := by
  refine ⟨?injective, ?surjective⟩
  case injective =>
    rw [← @MonoidHom.ker_eq_bot_iff]
    rw [@eq_bot_iff]
    intro k k_in_ker
    simp [PSL_monoidHom_PGL] at k_in_ker
    rw [← @QuotientGroup.mk_one] at k_in_ker
    -- extract representative or equivalent somehow
    rw [← @MulActionHom.toQuotient_apply] at k_in_ker
    -- show representative is a power of a primitive root of unity
    rw [mem_bot]
    rw [← @QuotientGroup.mk_one]
    sorry
  case surjective =>
    intro pgl
    -- extract representative or equivalent somehow
    -- obtain ⟨c, S, h⟩ := exists_SL_eq_scaled_GL_of_IsAlgClosed G
    sorry


noncomputable def PGL_iso_PSL (n F : Type*) [Fintype n] [DecidableEq n] [Nonempty n] [Field F] [IsAlgClosed F] :
PSL n F ≃* PGL n F := MulEquiv.ofBijective (PSL_monoidHom_PGL n F) (Bijective_PSL_monoidHom_PGL n F)

end Isomorphism

[Artie Khovanov]

I haven't done this myself but I'd start by looking for helper lemmas around *.lift

[Alex Brodbelt]

Ok will look at that, and what are you thinking when you think of a term of a quotient type? How does it behave?

[Artie Khovanov]

Well informally I'll think of it as an arbitrary representative. But eg if you have f:R->S "lifting" to fbar:R/I->S/J, showing [x] in S/J has a preimage is the same as finding y in R such that f(y)-x is in J. That's the sort of lemma I'd look for.

[Artie Khovanov]

Or in other words find your y with this property first, then lift it to the quotient using whatever lemmas about Quotient.lift (ie the universal property)

[Alex Brodbelt]

Yes, it is finding this $y$ I am struggling with, but at least I am beggining to see the big picture. Thanks

[Artie Khovanov]

Well you said you were stuck with a term of type PSL/PGL. I'm saying I would prove a statement of the form "for all x in GL there exists a y in SL such that..", then use the universal property to lift it.

[Alex Brodbelt]

I have that lemma (exists_SL_eq_scaled_GL_of_IsAlgClosed), but I don't know yet how to get the term of GL. Nonetheless, I'll try what you say.

[Artie Khovanov]

Oh I see
Yeah unfortunately any way you slice it you still have to use choice to take the nth root. It's just a bit easier when you're not making it be data ime.

[Alex Brodbelt]

When I see that I need to plug in a term of type α ⧸ s → Prop this means I should have x : _and x ∈ α ⧸ s where _ is ?? .

In particular, I am looking at docs#QuotientGroup.exists_mk

[Artie Khovanov]

No, x is of type α/s, there's no set involved

[Artie Khovanov]

Just like with any other function type

[Artie Khovanov]

But yes that's the sort of theorem I mean

[Alex Brodbelt]

It is docs#Quotient.exists_rep - Have proved surjectivity!

[Alex Brodbelt]

Have proved injectivity!

[Alex Brodbelt]

Thanks @Artie Khovanov :thanks:

[Kevin Buzzard]

@Alex Brodbelt I should also thank you -- your comments prompted me to write a blog post about how Lean thinks about quotients (something I've been meaning to do for ages), and I've finished it today, but I'm currently hesitant to post it because I mention NNG in it and right now the NNG website seems to be down.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2025/02/09/what-is-a-quotient/

[Edward van de Meent]

Unfortunately they also decided to write their diagrams upside-down so we are stuck with calling $s$ the “lift” of $\tilde{s}$.

:rolling_on_the_floor_laughing:

[Kevin Buzzard]

I still remember how horrified Patrick and I were when it dawned on us that lift meant "descent". On discussion with people Sebastian Ullrich the conclusion seemed to be that mathematicians thought that quotients should go under the object because they were smaller, and computer scientists thought that they should go above the object because they were more complex (they contained the original type and more besides). In category theory we sometimes just ignore the lift thing and call various universal things .desc.

[Edward van de Meent]

honestly, i can see how one might decide to call "turning a thing about Foo into a thing about a construction based on Foo" "lifting"

[Edward van de Meent]

because you might be doing some heavy lifting

[Kevin Buzzard]

Unfortunately "descent" is now baked into mathematical folklore and it's one of several reasons why mathematicians find quotients hard to use in lean; this is why I mentioned it. I didn't even go into the fact that it's also very difficult to translate between x \~~ y and "the formula you actually used to define the equivalence relation"...

[Alex Brodbelt]

To begin with the case split for what the finite subgroup of $\textrm{SL}_2(F)$ might look like I need to construct the so called maximal abelian subgroup class equation (harnesses the fact that centralizers of $\textrm{SL}_2(F)$ are isomorphic to nice subgroups), but to do this I first need to define the "non-central conjugacy class of a subgroup" (see the https://alexbrodbelt.github.io/ClassificationOfFiniteSubgroupsOfPGL/blueprint/Ch6_MaximalAbelianSubgroupClassEquation.html) the section 6.3 Conjugacy of Maximal Abelian Subgroups.

But the issue I am having is that docs#ConjClasses is not quite a set where I can take out the center as it directly defines a Quotient type. I am wondering how I should set up my definitions so it is not as painful to get the class equation to pop out.

There are some details I am still wrapping my head around to get the informal maths to correspond to formal maths but I figure I would start here, to at least get some ideas down.

Edit: (more context and better questions)

Let $\mathfrak{M}$ is the set of maximal abelian subgroups of $G$, the finite subgroup of $\textrm{SL}_2(F)$ to be classified, let $A \in \mathfrak{M}$ then the non-central part of $A$ is $A^* = A \setminus Z(\textrm{SL}_2(F))$.

Let $\mathfrak{M}^* := \{ A_i^* \; | \; A_i \in \mathfrak{M} \}$

For a given $A_i$, the conjugacy class of $A_i$ is defined as $\mathcal{C}_i = \{x A_i x^{-1} \; |\; x \in G \}$ (this is not quite docs#ConjClasses).

Similarly, let $\mathcal{C}_i* = \{x A_i^* x^{-1} \; | \; x \in G \}$. The nice property now is that the $\mathcal{C}_i^*$ partition $\mathfrak{M}^*$ as it is the equivalence class of $A_i^*$ in $\mathfrak{M}*$.

Then define $C_i^* = \cup_{x \in G} x A_i^* x^{-1}$, every element of $G \setminus Z(\textrm{SL}_2(F))$ lie within one of the $C_i^*$ as suppose $a_i \in A_i^*$ then there exists a $y \in G$ such that $y a_i y^{-1}$ as the map $f_y : G \rightarrow G$ defined by $x \mapsto y x y^{-1}$ defines an automorphism, so restricting to $G \setminus Z(\textrm{SL}_2(F)$ defines a bijection, because if $x, y \in G \setminus Z$ then $y x y^{-1} G \setminus Z$ . If $y x y^{-1} \in Z$ then there is a $z \in Z$ such that $z y x y^{-1} = 1 \iff y z x = y \iff x = z^{-1} \in Z$ a contradiction.

We also have the relation $|C_i^*| = |A_i*| |\mathcal{C}_i*|$.

That is to say, there exists an indexing set $S$ (not sure how I would construct such a set or sidestep this construction yet) where:

$G \setminus Z(\textrm{SL}_2(F)) = \bigcup_{i \in S} C_i^*$ (A)

I wonder if I should set up $C_i^*$ as having type Set or I should fiddle a little bit with the approach to set up a Quotient type....

From looking at the proof it seems sensible to define them as sets and maybe use something like docs#Finpartition.sum_card_parts on (A) to yield

$|G \setminus Z(\textrm{SL}_2(F))| = \sum_{i \in S} |C_i^*|$

[Kevin Buzzard]

What does "the non-central part of A" mean? What is \M? Can you ask a self-contained question?

[Artie Khovanov]

@Alex Brodbelt how about conjugatesOf and ConjClasses.carrier?

[Artie Khovanov]

In general going to the definition that doesn't quite work and poking around a bit often gets you what you want. Didn't try the AI tools as am on phone but I'd be surprised if they didn't suggest this, too.

[Artie Khovanov]

Like, you know you want the type to be Set G, so I imagine mentioning "sets" would get you there.

[Alex Brodbelt]

I was thinking something like this too, i.e tweaking an existing definition. But if I could avoid doing this that would be ideal.

So far I am thinking of defining all of these as sets $C_i*$ and proving that there is an equivalence relation on them which should then give me the partition of $G\setminus Z(\textrm{SL}_2(F))$.

p.s: have made the question more self-contained - sorry I was a bit lazy when I wrote it.

[Kevin Buzzard]

Re "this is not quite docs#ConjClasses" -- this is not at all docs#ConjClasses, that's "the type of all conjugacy classes of elements in a group", not "one conjugacy class associated to a set".

[Kevin Buzzard]

By $A \backslash Z$ I'm assuming that you literally mean the subset ("A minus Z"), not some quotient. Whatever it means, I still can't make your claim that the $C_i^*$ partition $G \backslash Z$ typecheck. You have defined $C_i^*$ to be a set of sets, not a set of elements, and for a bunch of sets to be a partition of a subset of a group they need to be sets of elements. What am I missing?

[Alex Brodbelt]

Apologies! it indeed does not type-check (I like this way of thinking about it hehe) - I think I fixed it. Will check it over again just in case.

[Kevin Buzzard]

With the revised version I should think that the $C_i^*$ have type Set (SL_2(F)).

[Kevin Buzzard]

Or possibly type Set G depending on what you want to do with them. Without more context it's hard to know.

[Alex Brodbelt]

I think I'll have to see what clicks, but at least figuring out I want to use Set is a good start! Thanks - Just wanted to consider options rather than jump straight in and then have to backtrack.

[Alex Brodbelt]

So far so good, I leave definitions in case something looks not so nice. But as somewhat anticipated, there is an issue with stating one of the key theorems:

I am not sure how to define the indexing set $S$ which comes from the fact that $C_i^*$ partition $G \setminus Z(\textrm{SL}_2(F)$. The critical theorem I would like to state is:

$|G \setminus Z(\textrm{SL}_2(F)| = \sum_{i \in S} |C_i^*|$ where $\bigcup_{i \in S} \mathcal{C}_i^* = \mathfrak{M}^*$

Recall $\mathcal{C}_i = \{x A_i x^{-1} \; | \; x \in G \}$ and $C_i^* = \bigcup{x \in G} x A_i x^{-1}$.

My guess so far is that $S$ or the subset $\{A_i | i \in S\}$ will come from the equivalence relation and the assumption that $S$ is finite, as $G$ is finite, $G \setminus Z(\textrm{SL}_2(F)$ is finite; so $|S| \leq |G \setminus Z(\textrm{SL}_2(F))|$ as $|C_i^*| > 0$.

But I'm not sure how I will convince lean of this, or how to get this indexing set $S$.

Code

import Mathlib

open Matrix MatrixGroups Subgroup MulAut Pointwise

def IsMaximalAbelian {L : Type*} [Group L] (G : Subgroup L) : Prop := Maximal (IsCommutative) G

def MaximalAbelianSubgroups { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
  { K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}

/- The non-central part of a subgroup -/
def Subgroup.noncenter {G : Type*} [Group G] (H : Subgroup G) : Set G :=
  {x : G | x ∈ H.carrier \ center G}

/- let M∗ be the set of all Aᵢ* and let Cᵢ* be the conjugacy class of Aᵢ* .-/
def noncenter_MaximalAbelianSubgroups {F : Type*} [Field F] (G : Subgroup SL(2,F)) :=
  { noncenter (K : Subgroup SL(2,F)) | K ∈ MaximalAbelianSubgroups G }


/-
Definition. The set $\mathcal{C}(A) = Cl(A) = \{x A x^{-1} \; | \; x ∈ G \}$
is called the conjugacy class of $A \in \mathcal{M}$.
-/
def ConjClassOfSet {G : Type*} [Group G] (A : Subgroup G) :=
  { conj x • A | x : G }

def noncenter_ConjClassOfSet {G : Type*} [Group G] (A : Subgroup G)  :=
  { conj x • noncenter A | x : G }

/-
Define the equivalence relation $\sim$ on $\mathcal{M}^*$ by
$A_i \sim A_j$ if and only if $A_i = x A_j x^{-1}$ for some $x \in G$.
 -/
instance {F : Type*} [Field F] {G : Subgroup SL(2,F)} :
  Setoid (noncenter_MaximalAbelianSubgroups G) where
  r Aᵢ Aⱼ := IsConj Aᵢ.val Aⱼ.val
  iseqv := {
    refl _x := ConjClasses.mk_eq_mk_iff_isConj.mp rfl,
    symm {_x _y} h := IsConj.symm h,
    trans {_x _y _z} h₁ h₂ := IsConj.trans h₁ h₂
    }

/-
Define $C (A)^* = \bicup_{x \in G} x A  x^{-1}$
-/
def noncenter_C {F : Type*} [Field F] (A G : Subgroup SL(2,F)) [Finite G] :=
  ⋃ x ∈ G, conj x • noncenter A

/-
We have the relation $|C_i^*| = |A_i^*| |\mathcal{C}_i^*|$
-/
lemma card_noncenter_C_eq_card_A_mul_card_noncenter_ConjClass {F : Type*} [Field F]
  (G A : Subgroup SL(2,F)) [Finite G] :
  Nat.card (noncenter_C A G) =
    Nat.card (noncenter A) * Nat.card (noncenter_ConjClassOfSet A) := by sorry

/-
$G \setminus Z(\textrm{SL}_2(F)) = \bigcup_{A \in \mathcal{M}} (C A)^*$
 -/
lemma subgroup_sdiff_center_eq_union_noncenter_C {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [Finite G] : G.carrier \ center (SL(2,F)) =
    ⋃ A ∈ MaximalAbelianSubgroups G, noncenter_C A G := by sorry

/-
$|\mathcal{C}_i| = |C_i|$
-/
lemma card_noncenter_ConjClassOfSet_eq_card_ConjClassOfSet {G : Type*} [Group G] (A : Subgroup G) :
  Nat.card (ConjClassOfSet A) = Nat.card (noncenter_ConjClassOfSet A) := by sorry

/-
$|\mathcal{C}_i| = [G : N_G(A_i)]$
-/
lemma card_ConjClassOfSet_eq_index_normalizer {F : Type*} [Field F] (A G : Subgroup SL(2,F)) :
  Nat.card (ConjClassOfSet A) = index (normalizer (A.subgroupOf G)) := by sorry

instance {L : Type*} [Group L] {G : Subgroup L} [Finite G] : Fintype (MaximalAbelianSubgroups G) := by sorry

-- theorem card_noncenter_fin_subgroup_eq_sum_card_noncenter_mul_index_normalizer {F : Type*} [Field F] (G : Subgroup SL(2,F))  :
--   Nat.card (G.carrier \ (center SL(2,F)).carrier : Set SL(2,F)) = ∑ A ∈ (MaximalAbelianSubgroups G), Nat.card A * index (normalizer (A.subgroupOf G)) := by sorry
-- NEED HELP DEFINING THIS STATEMENT - it is a stub at the minute

[Alex Brodbelt]

After discussions with Artie, I think the best way is again to lift some appropriate functions ...no need to faff around with silly sets.

[Artie Khovanov]

In general the concept of an "indexing set' is a formalisation red flag

[Alex Brodbelt]

This is what it looks like so far - I have lifted the function which computes the cardinality of the noncentral part of a maximal abelian subgroup.

import Mathlib
-- import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S2_SpecialSubgroups
-- import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S2_MaximalAbelianSubgroup

set_option maxHeartbeats 0
set_option linter.style.longLine true


variable {R F : Type*} [CommRing R] [Field F]

open Matrix MatrixGroups Subgroup MulAut Pointwise

def IsMaximalAbelian {L : Type*} [Group L] (G : Subgroup L) : Prop := Maximal (IsCommutative) G

def MaximalAbelianSubgroups { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
  { K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}


lemma MaximalAbelianSubgroup.center_le {G : Type u_1} [Group G] (H A : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups H)
  (hH : center G ≤ H) : center G ≤ A := by sorry

def Z (R : Type*) [CommRing R] : Subgroup SL(2,R) := closure {(-1 : SL(2,R))}

lemma center_SL2_eq_Z (R : Type u_1) [CommRing R] [NoZeroDivisors R] : center SL(2, R) = Z R := by sorry

lemma mem_Z_iff {R : Type*} [CommRing R] {x : SL(2,R)}: x ∈ Z R ↔ x = 1 ∨ x = -1 := by sorry

instance : Finite (Z F) := by
  simp only [mem_Z_iff]
  exact Finite.Set.finite_insert 1 {-1}
/- The non-central part of a subgroup -/
def Subgroup.noncenter {G : Type*} [Group G] (H : Subgroup G) : Set G :=
  {x : G | x ∈ H.carrier \ center G}


/-
We define the equivalence relation on the set of Maximal Abelian Subgroups of `G`, a finite
group of `SL(2,F)`
-/
instance MaximalAbelianSubgroups_lift {F : Type*} [Field F] (G : Subgroup SL(2,F)) :
  Setoid (MaximalAbelianSubgroups G) where
  r A B := ∃ (x : SL(2,F)), conj x • A.val = B.val
  iseqv := {
    refl A := ⟨1, by simp⟩
    symm := by
      rintro ⟨A, hA⟩  ⟨B, hB⟩ ⟨x, hx⟩
      use x⁻¹
      simp at hx ⊢
      rw [inv_smul_eq_iff]
      exact hx.symm
    trans := by
      rintro ⟨A, hA⟩ ⟨B, hB⟩ ⟨C, hC⟩ ⟨x, hx⟩ ⟨y, hy⟩
      use y * x
      rw [← hy, ← hx, smul_smul, MonoidHom.map_mul]
  }

noncomputable def card_noncenter_MaximalAbelianSubgroupsOf {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [Finite G] : MaximalAbelianSubgroups G → ℕ :=
  fun A => Nat.card ((A.val.carrier \ (center SL(2,F)).carrier) :)


lemma card_eq_of_related_noncenter_subgroups {F : Type*} [Field F] (G : Subgroup SL(2,F))
  (center_le_G : center SL(2,F) ≤ G)[ hG : Finite G] :
  ∀ (A B : (MaximalAbelianSubgroups G)),
    A ≈ B → card_noncenter_MaximalAbelianSubgroupsOf G A =
      card_noncenter_MaximalAbelianSubgroupsOf G B:= by
  rintro ⟨A, hA⟩ ⟨B, hB⟩ ArB
  simp only [← Quotient.eq_iff_equiv, Quotient.eq] at ArB
  obtain ⟨x, rfl⟩ := ArB
  simp only [card_noncenter_MaximalAbelianSubgroupsOf, center_toSubmonoid,
    Submonoid.center_toSubsemigroup, pointwise_smul_toSubmonoid, Set.Nat.card_coe_set_eq]
  let center_finite : Finite (center SL(2, F)) := by
    rw [center_SL2_eq_Z]
    infer_instance
  have center_le_A : (Subsemigroup.center SL(2, F)).carrier ⊆ A.carrier :=
    @MaximalAbelianSubgroup.center_le SL(2,F) _ G A hA center_le_G
  let center_coe_finite : Finite (Subsemigroup.center SL(2, F)).carrier := center_finite
  have center_le_conj_A :
    (Subsemigroup.center SL(2, F)).carrier ⊆ (conj x • A.toSubmonoid).carrier := by
    intro z hz
    rw [Submonoid.mem_carrier, Submonoid.mem_pointwise_smul_iff_inv_smul_mem]
    have hz' := hz
    rw [Subsemigroup.mem_carrier, Subsemigroup.mem_center_iff] at hz'
    simp only [MulAut.smul_def, conj_inv_apply, mem_toSubmonoid]
    rw [hz' x⁻¹]
    group
    exact center_le_A hz
  rw [Set.ncard_diff center_le_A, Set.ncard_diff center_le_conj_A]
  have key : (conj x • A.toSubmonoid).carrier.ncard = A.carrier.ncard := by
    symm
    refine Set.ncard_congr (fun a ha ↦ x * a * x⁻¹) ?closure ?injective ?surjective
    case closure =>
      intro a ha
      simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup,
        Submonoid.mem_pointwise_smul_iff_inv_smul_mem,
        smul_mul', MulAut.smul_def, conj_inv_apply, inv_mul_cancel, one_mul, smul_inv',
        mem_toSubmonoid]
      group
      exact ha
    case injective =>
      intro a b ha hb hab
      simp only [mul_left_inj, mul_right_inj] at hab
      exact hab
    case surjective =>
      rintro b ⟨y, hy, rfl⟩
      use y, hy
      congr
  rw [key]

/-
We lift the function which computes the cardinality of the noncentral part of a maximal subgroup
-/
noncomputable def lift_card {F : Type*} [Field F] (G : Subgroup SL(2,F))
  (center_le_G : center SL(2,F) ≤ G) [Finite G] :=
  @Quotient.lift _ _ (s := MaximalAbelianSubgroups_lift G)
    (f := card_noncenter_MaximalAbelianSubgroupsOf G)
    (card_eq_of_related_noncenter_subgroups G center_le_G)

[Alex Brodbelt]

The above was just in case someone spots something awful that should be different.

[Alex Brodbelt]

1) I am trying to state the final theorem for the classification of finite subgroups of $\textrm{SL}_2(F)$ and the last group I am trying to define is a bit strange as I need to embed $\mathbb{F}_{p^k}$ into $\mathbb{F}_{p^{2k}}$

image.png

I want to imitate how $\mathbb{F}_{p^k}$ the Galois Field is defined to be the splitting field of $X^{p^k} - X \in \mathbb{F}_p[X]$ docs#GaloisField which then allows to understand the Galois Field as an $\mathbb{F}_p$-algebra.

In my case, am correct (in informal maths) to think $\mathbb{F}_{p^{2k}}$ is the splitting field of $X^{p^k} - X \in \mathbb{F_{p^k}}[X]$? And that (in formal maths) I am looking for the corresponding $\mathbb{F}_{p^k}$-algebra which will allows me to map $\mathbb{F}_{p^k}$ into $\mathbb{F}_{p^{2k}}$ and the subsequently define the "injection" of $\textrm{SL}_2(\mathbb{F}_{p^k})$ into $\textrm{SL}_2(\mathbb{F}_{p^{2k}})$?

Is this already defined or set up somewhere else? in case I don't have to rebuild (its already been invented, formalisation would be building(?) ...anyway I am rambling) the wheel.

[Alex Brodbelt]

2) Also, so far to make my final statement look pretty I am defining the following proposition:

import Mathlib

def Isomorphic (G H : Type*) [Group G] [Group H] :=
  ∃ φ : G ≃* H, True

It is a bit unfortunate I need to add the True term. But maybe I am not aware of some nice construct? Not a big issue anyway.

[Artie Khovanov]

For the last thing, you're just asking for an isomorphism. So the final statement you want is just, the definition of the isomorphism.

[Artie Khovanov]

Oh I guess you can do like, Nonempty G ~=* H

[Kevin Buzzard]

(probably Nonempty (G \equiv* H))

[Scott Carnahan]

There is exactly one ring homomorphism from a field with $p^k$ elements to a field with $p^{2k}$ elements, and you should be able to get it from the presentation as a splitting field of $X^{p^{2k}} - X$. (please disregard)

[Kevin Buzzard]

By Galois theory there are k ring homomorphisms.

[Damiano Testa]

I guess Scott meant that there is exactly one subfield with $p^k$ elements. This field has $k$ automorphisms.

[Scott Carnahan]

Let me try again. When working with algebraic groups over finite fields, you may find yourself with a finite field F and a quadratic extension K. While you can speak of K as a splitting field (unique up to isomorphism) of a specific large polynomial, in practice it is almost always better to assert that K = F[r] for some F-irrational element r of K. You can get a lot done by reasoning with the coefficients of its minimal polynomial in F, which up to sign are the trace and norm.

[Alex Brodbelt]

I somewhat follow the reasoning, I am not sure how to get the desired homomorphism from $\mathbb{F}_{p^k} \rightarrow \mathbb{F}_{p^{2k}}$ in Lean.

I am not familiar with the Galois theory part of mathlib - and I am doing a Galois theory course at the moment so I am by no means an expert.

The definition of splitting field in mathlib looks quite unwieldy to me, I expect there is some more elementary theorem which is more suitable for my purposes.

[Kevin Buzzard]

Can you formalize your question in Lean? I'm not clear which finite field you actually need in your application. Otherwise someone might come up with some code and say "this is the mathematical statement you want" and your response might be "yeah but cour code doesn't apply in my situation".

[Alex Brodbelt]

I want to define the group homomorphism below because I need to define the (normal) subgroup $\langle \textrm{SL}_2(F_{p^k}), d_\pi \rangle \lhd \textrm{SL}_2(F_{p^{2k}})$ where $\pi \in F_{p^{2k}} \setminus F_{p^k}$ and $\pi^2\in F_{p^k}$.

This is one of the cases of what $G$ the finite subgroup of $\textrm{SL}_2(F)$ is isomorphic to.

import Mathlib

open Subgroup MatrixGroups

def ringHom {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ+}:
  GaloisField p k →+* GaloisField p (2*k) := sorry

-- (x) The group hSL(2, Fq ), dπ i, where SL(2, Fq ) C hSL(2, Fq ), dπ i.
def monoidHom {R S : Type*} [CommRing R] [CommRing S] :
  SL(2, R) →* SL(2, S) where
  toFun A := sorry
  map_one' := sorry
  map_mul' := sorry

then I do map monoidHom (⊤ :SL(2, GaloisField p k)) ⊔ closure (d π)

[Scott Carnahan]

I think I see the problem: mathlib4 doesn't have any specialized API for extensions of finite fields yet. One possible path is to take fixed points of the p^k power map on GaloisField p (2 * k), and show that it is a splitting field of X ^ (p ^ k) - X. Then you get existence of an isomorphism from GaloisField p k.

[Johan Commelin]

But that def monoidHom should be done for SL(n, R) -> SL(n, S) for arbitrary ring homs R -> S.

[Johan Commelin]

In other words: I encourage you to split this into two smaller targets.

[Alex Brodbelt]

this was my thought too - will update MWE

[Yakov Pechersky]

Something like?

import Mathlib

variable {p : ℕ} [Fact (Nat.Prime p)] {K L : Type*} [Field K] [Field L]
  [Algebra (ZMod p) K] [Algebra (ZMod p) L] [Finite K]

noncomputable
def inclusion (h : Nat.card K ≤ Nat.card L) :
    K →ₐ[ZMod p] L := by
  let k := Nat.log p (Nat.card K)
  let l := Nat.log p (Nat.card L)
  have hk : Nat.card K = p ^ k := sorry
  have hl : Nat.card L = p ^ l := sorry
  let e : K ≃ₐ[ZMod p] GaloisField p k := GaloisField.algEquivGaloisField _ _ hk
  let e' : L ≃ₐ[ZMod p] GaloisField p l := GaloisField.algEquivGaloisField _ _ hl
  let hb := Basis.exists_basis (ZMod p) (GaloisField p k)
  let ι := hb.choose
  let b := Classical.choice hb.choose_spec
  let hbf : Fintype ι := FiniteDimensional.fintypeBasisIndex b
  let hb' := Basis.exists_basis (ZMod p) (GaloisField p l)
  let ι' := hb'.choose
  let b' := Classical.choice hb'.choose_spec
  let hbf' : Fintype ι' := FiniteDimensional.fintypeBasisIndex b'
  have : Fintype.card ι ≤ Fintype.card ι' := sorry
  let f : ι → ι' := sorry
  have hf : Function.Injective f := sorry
  refine {
    toFun x := e'.symm (Basis.constr b (ZMod p) (fun i ↦ b'.equivFun.symm (fun i' ↦ sorry)) (e x))
    map_one' := sorry
    map_mul' := sorry
    map_zero' := sorry
    map_add' := sorry
    commutes' := sorry
  }

[Yakov Pechersky]

not very familiar with Basis API

[Alex Brodbelt]

Ohhhhh

[Kevin Buzzard]

and your monoidHom is docs#Matrix.SpecialLinearGroup.map

[Kevin Buzzard]

@Yakov Pechersky

import Mathlib

variable {p : ℕ} [Fact (Nat.Prime p)] {K L : Type*} [Field K] [Field L]
  [Algebra (ZMod p) K] [Algebra (ZMod p) L] [Finite K]

noncomputable
def inclusion (h : Nat.card K ≤ Nat.card L) :
    K →ₐ[ZMod p] L := by
...

isn't correct. If p is prime, if $K$ has size $p^2$ and if $L$ has size $p^3$ then there's no map from $K$ to $L$ because any such map would make $L$ into a $K$-vector space of dimension $3/2$. The correct claim is that for $k,n>0$ there are $k$ $\mathbb{Z}/p\mathbb{Z}$-algebra homs from $GF(p^k)$ to $GF(p^n)$ if $k|n$ and none otherwise.

[Alex Brodbelt]

Thanks! I am stubbing out everything so I can define all statements and dependencies and have nice looking dependency graph - so this will do for now :-)

[Alex Brodbelt]

For hopefully the last thing I need to stub out - The maximal abelian class equation

I have defined an equivalence relation on the set of maximal abelian subgroups of $G$, $\mathfrak{M}$ (the definition should not matter too much - it is in the code if you need it) - this yields a Setoid $\mathfrak{M} / \sim$

where $A \sim B$ if and only if $\exists x \in G, x A x^{-1} = B$

I have defined a function card_noncenter : MaximalAbelianSubgroups G → ℕ defined by
$A \mapsto |A \setminus Z(\textrm{SL}_2(F))|$

I have lifted this function as the function card_noncenter respects the equivalence relation/well-defined.

Now, all my effort is toward being able to state (caveat: the formula is not quite right it needs another term multiplying the sums):

$|G \setminus Z(\textrm{SL}_2(F))| = \sum_{ A \in \mathfrak{M} / \sim } \textrm{card\textunderscore noncenter}(A)$

I have shown the Quotient defined from the Setoid can be promoted to Fintype as I have shown finiteness of the quotient.

but when I plug in the function into the sum over the fintype it is not happy with me summing natural numbers (the cardinality of the noncentral part of the equivalence relations) - it is expecting a Sort? I am not sure why?

Code

import Mathlib

set_option maxHeartbeats 0
set_option linter.style.longLine true


variable {R F : Type*} [CommRing R] [Field F]

open Matrix MatrixGroups Subgroup MulAut Pointwise

def IsMaximalAbelian {L : Type*} [Group L] (G : Subgroup L) : Prop := Maximal (IsCommutative) G

def MaximalAbelianSubgroups { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
  { K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}

/- The non-central part of a subgroup -/
def Subgroup.noncenter {G : Type*} [Group G] (H : Subgroup G) : Set G :=
  {x : G | x ∈ H.carrier \ center G}

/- let M∗ be the set of all Aᵢ* and let Cᵢ* be the conjugacy class of Aᵢ* .-/
def noncenter_MaximalAbelianSubgroups {F : Type*} [Field F] (G : Subgroup SL(2,F)) :=
  { noncenter (K : Subgroup SL(2,F)) | K ∈ MaximalAbelianSubgroups G }


/-
We define the equivalence relation on the set of Maximal Abelian Subgroups of `G`, a finite
group of `SL(2,F)`
-/
instance MaximalAbelianSubgroups_lift {F : Type*} [Field F] (G : Subgroup SL(2,F)) :
  Setoid (MaximalAbelianSubgroups G) where
  r A B := ∃ (x : SL(2,F)), conj x • A.val = B.val
  iseqv := {
    refl A := ⟨1, by simp⟩
    symm := by
      rintro ⟨A, hA⟩  ⟨B, hB⟩ ⟨x, hx⟩
      use x⁻¹
      simp at hx ⊢
      rw [inv_smul_eq_iff]
      exact hx.symm
    trans := by
      rintro ⟨A, hA⟩ ⟨B, hB⟩ ⟨C, hC⟩ ⟨x, hx⟩ ⟨y, hy⟩
      use y * x
      rw [← hy, ← hx, smul_smul, MonoidHom.map_mul]
  }

noncomputable def card_noncenter_MaximalAbelianSubgroupsOf {F : Type*} [Field F]
  (G : Subgroup SL(2,F)) [Finite G] : MaximalAbelianSubgroups G → ℕ :=
  fun A => Nat.card ((A.val.carrier \ (center SL(2,F)).carrier) :)


lemma card_eq_of_related_noncenter_subgroups {F : Type*} [Field F] (G : Subgroup SL(2,F))
  (center_le_G : center SL(2,F) ≤ G)[ hG : Finite G] :
  ∀ (A B : (MaximalAbelianSubgroups G)),
    A ≈ B → card_noncenter_MaximalAbelianSubgroupsOf G A =
      card_noncenter_MaximalAbelianSubgroupsOf G B:= by sorry

/-
We lift the function which computes the cardinality of the noncentral part of a maximal subgroup
-/
noncomputable def lift_card_noncenter {F : Type*} [Field F] (G : Subgroup SL(2,F))
  (center_le_G : center SL(2,F) ≤ G) [Finite G] :=
  @Quotient.lift _ _ (s := MaximalAbelianSubgroups_lift G)
    (f := card_noncenter_MaximalAbelianSubgroupsOf G)
    (card_eq_of_related_noncenter_subgroups G center_le_G)

open Function

lemma Injective_subroup_to_subset {L : Type*} [Group L] (G : Subgroup L) [Finite G] :
  Injective
    (fun (H : {K | (K : Subgroup L) ≤ G}) =>
      (⟨H.val.carrier, H.property⟩ : {K | K ⊆ G.carrier})) := by
  sorry

instance finite_MaximalAbelianSubgroups {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [hG : Finite G] : Set.Finite (MaximalAbelianSubgroups G) := by
  sorry

instance finite_MaximalAbelianSubgroups' {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [hG : Finite G] : Finite (MaximalAbelianSubgroups G) :=
    Set.finite_coe_iff.mpr <| finite_MaximalAbelianSubgroups G

instance finite_MaximalAbelianSubgroups_lift {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [hG : Finite G] : Finite (Quotient (MaximalAbelianSubgroups_lift G)) := Quotient.finite _


noncomputable instance fintype_MaximalAbelianSubgroups_lift {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [hG : Finite G] : Fintype (Quotient (MaximalAbelianSubgroups_lift G)) := by
  sorry

example {F : Type*} [Field F] (G : Subgroup SL(2,F)) (center_le_G : center SL(2,F) ≤ G)
  [hG : Finite G] : ∑ A_lift : Quotient (MaximalAbelianSubgroups_lift G), (lift_card_noncenter G center_le_G) A_lift  := by sorry

[Ruben Van de Velde]

It seems to be complaining that the sum is not a proposition; if you add = 0 before the :=, it works

[Alex Brodbelt]

Oh of course :clown: - sorry

[Ruben Van de Velde]

No worries

[Yakov Pechersky]

I apologize for the misleading snippet above. Here's another attempt for a general algHom, not one that necessarily has the properties you want.

import Mathlib

open Polynomial

variable {p : ℕ} [Fact (Nat.Prime p)] {n m : ℕ}

variable (p n) in
protected noncomputable
abbrev GaloisField.polynomial : (ZMod p)[X] := X ^ p ^ n - X

lemma GaloisField.polynomial_ne_zero : GaloisField.polynomial p n ≠ 0 := by
  rw [GaloisField.polynomial]
  sorry

lemma GaloisField.splits_of_dvd (hn : n ∣ m) :
    Splits (algebraMap (ZMod p) (GaloisField p m)) (GaloisField.polynomial p n) := by
  have hsk : Splits (algebraMap (ZMod p) (GaloisField p m)) (GaloisField.polynomial p m) :=
    IsSplittingField.splits (GaloisField p m) (GaloisField.polynomial p m)
  have hsk' : Splits (algebraMap (ZMod p) (GaloisField p m)) (X ^ (p ^ m - 1) - 1) := by
    refine splits_of_splits_of_dvd _ polynomial_ne_zero hsk ⟨X, ?_⟩
    suffices (X : (ZMod p)[X]) ^ p ^ m = X ^ (p ^ m - 1 + 1) by
      simpa [GaloisField.polynomial, sub_mul, ← pow_succ]
    rw [tsub_add_cancel_of_le]
    exact Nat.pow_pos (Nat.Prime.pos Fact.out)
  obtain ⟨k, rfl⟩ := hn
  have hd : (p ^ n - 1) ∣ (p ^ (n * k) - 1) := by sorry
  have hdx : (X : (ZMod p)[X]) ^ (p ^ n - 1) - 1 ∣ X ^ (p ^ (n * k) - 1) - 1 := by sorry
  have hs' : Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (X ^ (p ^ n - 1) - 1) := by
    refine splits_of_splits_of_dvd _ ?_ hsk' hdx
    sorry
  have hs : Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (GaloisField.polynomial p n) := by
    rw [GaloisField.polynomial]
    suffices Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (X * (X ^ (p ^ n - 1) - 1)) by
      convert this using 1
      sorry
    rw [splits_mul_iff]
    exact ⟨splits_X _, hs'⟩

noncomputable
def GaloisField.algHom_of_dvd (hn : n ∣ m) : GaloisField p n →ₐ[ZMod p] GaloisField p m :=
  Polynomial.SplittingField.lift _ (splits_of_dvd hn)

[Alex Brodbelt]

Wow! thank you! - filled in the remaining sorries!

[Yakov Pechersky]

Please PR these!

[Alex Brodbelt]

Will do! (but after submitting my thesis this Tuesday)

In the meantime, if anyone wants to golf the following:

Code

import Mathlib

open Polynomial

/- Embed GF(p^k) into GF(p^m) where k ∣ m -/
variable {p : ℕ} [hp : Fact (Nat.Prime p)] {n m : ℕ+}

variable (p n) in
protected noncomputable
abbrev GaloisField.polynomial : (ZMod p)[X] := X ^ p ^ n.val - X


lemma GaloisField.polynomial_ne_zero : GaloisField.polynomial p n ≠ 0 := by
  rw [GaloisField.polynomial]
  exact FiniteField.X_pow_card_pow_sub_X_ne_zero (ZMod p) n.ne_zero hp.out.one_lt

lemma GaloisField.splits_of_dvd (hn : n ∣ m) :
    Splits (algebraMap (ZMod p) (GaloisField p m)) (GaloisField.polynomial p n) := by
  have hsk : Splits (algebraMap (ZMod p) (GaloisField p m)) (GaloisField.polynomial p m) :=
    IsSplittingField.splits (GaloisField p m) (GaloisField.polynomial p m)
  have hsk' : Splits (algebraMap (ZMod p) (GaloisField p m)) (X ^ (p ^ m.val - 1) - 1) := by
    refine splits_of_splits_of_dvd _ polynomial_ne_zero hsk ⟨X, ?_⟩
    suffices (X : (ZMod p)[X]) ^ p ^ m.val = X ^ (p ^ m.val - 1 + 1) by
      simpa [GaloisField.polynomial, sub_mul, ← pow_succ]
    rw [tsub_add_cancel_of_le]
    exact Nat.pow_pos (Nat.Prime.pos Fact.out)
  obtain ⟨k, rfl⟩ := hn
  have hd : (p ^ n.val - 1) ∣ (p ^ (n.val * k) - 1) := by
    exact nat_pow_one_sub_dvd_pow_mul_sub_one p ↑n ↑k
  have hdx : (X : (ZMod p)[X]) ^ (p ^ n.val - 1) - 1 ∣ X ^ (p ^ (n.val * k) - 1) - 1 := by
    let  Y : (ZMod p)[X] := X ^ (p ^ n.val - 1)
    obtain ⟨m, hm⟩ := hd
    simp_rw [hm, pow_mul]
    suffices Y - 1 ∣ Y^m -1 by
      simp [Y] at this
      exact this
    exact sub_one_dvd_pow_sub_one Y m
  have hs' : Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (X ^ (p ^ n.val - 1) - 1) := by
    refine splits_of_splits_of_dvd _ ?_ hsk' hdx
    refine Monic.ne_zero_of_ne ?_ ?_
    exact zero_ne_one' (ZMod p)
    refine monic_X_pow_sub ?_
    simp [hp.out.one_lt]
  have hs : Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (GaloisField.polynomial p n) := by
    rw [GaloisField.polynomial]
    suffices Splits (algebraMap (ZMod p) (GaloisField p (n * k))) (X * (X ^ (p ^ n.val - 1) - 1)) by
      convert this using 1
      simp only [mul_sub, mul_one, sub_left_inj]
      nth_rewrite 2 [← pow_one X]
      rw [← pow_add, Nat.one_add, Nat.sub_one, Nat.succ_pred]
      exact Ne.symm (NeZero.ne' (p ^ n.val))
    rw [splits_mul_iff]
    exact ⟨splits_X _, hs'⟩
    exact X_ne_zero
    refine Monic.ne_zero_of_ne ?_ ?_
    exact zero_ne_one' (ZMod p)
    refine monic_X_pow_sub ?_
    simp [hp.out.one_lt]
  exact hs


noncomputable
def GaloisField.algHom_of_dvd (hn : n ∣ m) : GaloisField p n →ₐ[ZMod p] GaloisField p m :=
  Polynomial.SplittingField.lift _ (splits_of_dvd hn)