Project idea: GL_n(F_q)

Stream: LFTCM 2024

[Chris Birkbeck]

The idea is to find the size of $\mathrm{GL}_n(\mathbb{F}_q)$, which is $\prod_{i=0}^{n-1}(q^n-q^i) .$

[Chris Birkbeck]

If you would like to just copy-paste a start of this, you can make a new file (ask me if you need help with this) and then paste in:

import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup

open Matrix BigOperators

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

noncomputable instance fintype : Fintype (GL (Fin n) (GaloisField p m)) := by
    exact Fintype.ofFinite (GL (Fin n) (GaloisField p m))

lemma card : Fintype.card (GL (Fin n) (GaloisField p m)) =
   ∏ i : (Fin n), (p ^ (n * m) - p ^ (n * i)) := by sorry

local notation "𝔽" => (GaloisField p m)

variable (v : Fin n → 𝔽)

#check Submodule.span 𝔽 ({v} : Set (Fin n → 𝔽))




--Basis.invertibleToMatrix might be useful to turn it into a question about bases.

[Peiran Wu]

Here is a proof I have in mind; no idea how doable it is.

1. Define a (non-canonical) bijection between the invertible matrices and the bases, thereby reducing the problem to counting the number of bases.
2. Define, given a non-zero vector v in V, a bijection between the bases of V starting with v and the bases of V / <v>.
3. Prove the result by induction on the dimension.

[Chris Birkbeck]

Ok so 1. is definitely doable. This is all in Basis.invertibleToMatrix. But we can talk more about this to do the precise statement. 2. sounds like a good idea, but maybe we need to think about the best way to state it. And then yes 3 should be easy.

[Peiran Wu]

As an alternative to 1., GL acts regularly on the set of all bases and docs#MulAction.orbitEquivQuotientStabilizer gives us the bijection. This will probably boil down to the same arguments, so is not a priority.

[Edgar Costa]

It would be nice if we could also make the argument work for $R= \mathbb{Z}/N \mathbb{Z}$, but that is not a priority

[Chris Birkbeck]

So I've made a repo for this: Hopefully following these instructions should let you download it:

git clone https://github.com/CBirkbeck/GLn_F_q
cd GLn_F_q
lake exe cache get
lake build

[Chris Birkbeck]

Peiran Wu said:

As an alternative to 1., GL acts regularly on the set of all bases and docs#MulAction.orbitEquivQuotientStabilizer gives us the bijection. This will probably boil down to the same arguments, so is not a priority.

Oh nice that could be useful. Its always good to have multiple options and see which is best for mathlib

[Chris Birkbeck]

Edgar Costa said:

It would be nice if we could also make the argument work for $R= \mathbb{Z}/N \mathbb{Z}$, but that is not a priority

Yes I agree this would be really nice! If there is a proof that isnt much harder then we could definitely think about this.

[Chris Birkbeck]

I propose we meet up after Amelia's talk this afternoon and we can chat about how to approach this!

[Peiran Wu]

The git repo has not been set-up correctly (.gitignore is old probably from prior to v4.3.0 and the inner modules are not imported into the main file so lake build doesn't do much). I've fixed this locally and can push the fix to a branch

[Peiran Wu]

Chris Birkbeck said:

I propose we meet up after Amelia's talk this afternoon and we can chat about how to approach this!

I'm up for this!

[Chris Birkbeck]

Peiran Wu said:

The git repo has not been set-up correctly (.gitignore is old probably from prior to v4.3.0 and the inner modules are not imported into the main file so lake build doesn't do much). I've fixed this locally and can push the fix to a branch

Oh thank you! yes push the fix and I'll merge it

[Peiran Wu]

OK, just need push access. My GitHub handle is wupr :)

[InnaCap]

Hi Guys, could I join you?

[InnaCap]

The only problem is I know nothing.

[Chris Birkbeck]

Yes! thats perfectly fine. We can talk about this after Amelia's talk :)

[InnaCap]

Great! Thank you very much. Where will I find you?

[Chris Birkbeck]

How about we meet up near the piano at the front on the room (by the boards), we can then maybe go find some room in the library/elsewhere

[Alessandro Iraci]

Suggestion: prove instead that the number of maximal rank $n \times r$ matrices with entries in $\mathbb{F}_q$ is $\prod_{i=0}^{r-1} (q^n - q^i)$, it should be a lot easier to do by induction.

[InnaCap]

Sorry, where is the piano?

[Chris Birkbeck]

Oh I just mean the covered up one at the front of the lecture theatre (although I'm not there yet, just snacking at the moment)

[Peiran Wu]

Orbit-stabilizer theorem: docs#MulAction.orbitEquivQuotientStabilizer

[Peiran Wu]

Alessandro Iraci said:

Suggestion: prove instead that the number of maximal rank $n \times r$ matrices with entries in $\mathbb{F}_q$ is $\prod_{i=0}^{r-1} (q^n - q^i)$, it should be a lot easier to do by induction.

One way to phrase this could be the following?

abbrev q := p ^ m

variable (v : Fin n → 𝔽)

lemma step2 (k : ℕ) (hk : k ≤ n) :
    Nat.card { s : Fin k → (Fin n → 𝔽) // LinearIndependent 𝔽 s } = ∏ i : Fin k, ((p ^ m) ^ n - (p ^ m) ^ i.val) :=
  sorry

[Thomas Lanard]

Some results about linear independent vectors

#check LinearIndependent
#check LinearIndependent.comp
#check linearIndependent_unique_iff
#check linearIndependent_fin_cons
#check linearIndependent_fin_snoc

[Thomas Lanard]

For the initialization

induction k
    · simp [LinearIndependent]

[Antoine Chambert-Loir]

It may be easier to talk about finite families of vectors (Fin m -> V) which are linearly independent. If m < n, any such family can be extended to a family (Fin (m+1) -> V) in exactly … ways, by choosing a vector which is not in the span.

[Peiran Wu]

I have just finished Step 2 (still a lot of tidying-up to do). The code is now on branch wupr of the project repo.

[Peiran Wu]

Antoine Chambert-Loir said:

It may be easier to talk about finite families of vectors (Fin m -> V) which are linearly independent. If m < n, any such family can be extended to a family (Fin (m+1) -> V) in exactly … ways, by choosing a vector which is not in the span.

Yes, that's exactly what I have done.

[Johan Commelin]

@InnaCap and I made some progress on Step 1 yesterday. We can push this to the repo.

[Peiran Wu]

I've merged my branch into main since everyone seems to be working there.

[Thomas Lanard]

I have finished step 1 and made the connection with step 2 to have a complete proof of the cardinal of GLn(Fq). However, I do not have the authorization to push to the repo.

[Chris Birkbeck]

Oh send me your GitHub username and I'll add you

[Chris Birkbeck]

Also, that's great!!

[Chris Birkbeck]

Sorry I didn't actually read what you said, so the project is done! thats amazing!

[Chris Birkbeck]

or at least done until the $\mathbb{Z}/N\mathbb{Z}$ people come back :P

[Thomas Lanard]

:)

[Kevin Buzzard]

How about the size of O_n(q)?

[Chris Birkbeck]

Hmm I don't remember what the proofs are in that case. I'll have to look.

[Antoine Chambert-Loir]

It's much more complicated, (un)fortunately and the answer has arithmetic content.
The only example I know by heart is for n = 2 : if -1 is a square in Fq, then it's q - 1, otherwise it's q + 1.
To do the proof for a general quadratic form, I'd take an orthogonal basis, and map the first vector to a vector of same value, hence I need to know the cardinality of the sphere, and I'd go on by induction. Fortunately, Witt tells you that orthogonals of two lines generated by vectors of same value are isomorphic.

[Thomas Lanard]

I pushed in the repo the proof of the cardinal of $GL_n(\mathbb{Z}/p^r\mathbb{Z})$.
It just remains to prove that $\text{card } GL_n(\mathbb{Z}/p\mathbb{Z}) = \text{card } GL_n(\mathbb{F}_p)$ and do some cleaning. (I will do it later)
I will also try to finish the cardinal of $GL_n(\mathbb{Z}/N\mathbb{Z})$ using the chinese remainder theorem.

[Chris Birkbeck]

Ah fantastic! its been a good train ride I see :)

[Riccardo Brasca]

Do we have that GL of isomorphic rings are isomorphic?

[Chris Birkbeck]

maybe not explicitly, but surely we have enough to do this.

[Johan Commelin]

It the proof is about $\text{GL}_n(K)$, and gives the result in terms of card K, then we don't need such a result.

[Chris Birkbeck]

Aha yes good point! Thats another good reason to not use GaloisField and instead use a "general" finite field :)

[Thomas Lanard]

Given a morphisme of commutative rings I defined in the file a morphism of group for GL. I don’t think it is too difficult to prove that this is a isomorphism.

[Chris Birkbeck]

Riccardo Brasca said:

Do we have that GL of isomorphic rings are isomorphic?

But if we dont have this, we should definitely add it, even if we dont need it here.

[Thomas Lanard]

If we want to use the chinese remainder theorem to get $GL_n(\mathbb{Z}/N\mathbb{Z})$ we need it I think.

[Riccardo Brasca]

Yes, I was thinking about the chinese remainder theorem.

[Riccardo Brasca]

If you need to add it, consider adding that GL preserve injectivity first.

[Riccardo Brasca]

Does anyone know a reasonable criterion to get surjectivity?

[Johan Commelin]

To preserve isoms, you only need functoriality

[Riccardo Brasca]

Sure, but since injectivity is clearly preserved we can also add it.

[Riccardo Brasca]

I was just curious about surjectivity (that is not preserved in general)

[Thomas Lanard]

Riccardo Brasca said:

Does anyone know a reasonable criterion to get surjectivity?

morphism surjective + x is a unit if f(x) is a unit?

[Johan Commelin]

Fun fact: such f are called local ring homs in Lean

[Riccardo Brasca]

ah sure, preserving units is also a necessary condition.

[Johan Commelin]

Except when n = 0 :stuck_out_tongue_wink:

[Chris Birkbeck]

Chris Birkbeck said:

Aha yes good point! Thats another good reason to not use GaloisField and instead use a "general" finite field :)

Ok this is done!

[Kevin Buzzard]

For SL_n it's much more subtle -- for example SL_n(Z) surjects into SL_n(Z/NZ) but this is not immediately obvious as far as i know

[Antoine Chambert-Loir]

Riccardo Brasca said:

Does anyone know a reasonable criterion to get surjectivity?

It's a good question. For GL, little hope, unless you have surjectivity on units of the rings, but for SL, you get it by adapting the proof that SL(n, Z) is generated by elementary matrices (1s one diagonal, 0 elsewhere except for one 1).

[Thomas Lanard]

I have an issue finishing the proof of the cardinal of $\text{GL}_n(\mathbb{Z}/N\mathbb{Z})$. So I want to rewrite N into its decomposition into prime numbers (in order to apply the Chinese Remainder Theorem). However, I have an error that I don’t understand. I think it has something to do with the instance of Fintype. Here are two attempts with a stupid example :

import Mathlib
open BigOperators

variable (N : ℕ) [NeZero N]

instance : Fintype (ZMod (N)) := ZMod.fintype N

noncomputable instance : Fintype (GL (Fin n) (ZMod (N))) := Fintype.ofFinite (GL (Fin n) (ZMod N))

lemma card_GL_ZMod : Fintype.card (GL (Fin n) (ZMod (N))) =  1 := by
  have h : N ≠ 0 := Ne.symm (NeZero.ne' N)
  rw [←(Nat.factorization_prod_pow_eq_self h)]
  --tactic 'rewrite' failed, motive is not type correct

Here the rewrite does not work (tactic 'rewrite' failed, motive is not type correct).

Second attempt :

import Mathlib
open BigOperators

variable (N : ℕ) (h : N ≠ 0)

noncomputable instance : NeZero N := by exact { out := h }

instance : Fintype (ZMod (N)) := by
  have : NeZero N := by exact { out := h }
  apply ZMod.fintype N

noncomputable instance : Fintype (GL (Fin n) (ZMod (N))) := by
  have : NeZero N := by exact { out := h }
  apply Fintype.ofFinite (GL (Fin n) (ZMod N))

lemma card_GL_ZMod : Fintype.card (GL (Fin n) (ZMod (N))) =  1 := by
  --failed to synthesize instance Fintype (GL (Fin n) (ZMod N))
  rw [←(Nat.factorization_prod_pow_eq_self h)]

This time Lean complains: failed to synthesize instance Fintype (GL (Fin n) (ZMod N))

[Johan Commelin]

The instance

instance : Fintype (ZMod (N)) := by
  have : NeZero N := by exact { out := h }
  apply ZMod.fintype N

can not be applied automatically, because it depends on the explicit variable h which Lean cannot find automatically. Idem dito for the other Fintype instance below it.

[Chris Birkbeck]

You could use (N : ℕ+) instead and then you dont need the NeZero stuff

[Chris Birkbeck]

Although I don't think it'll let you rewrite N in the Zmod N into Zmod (product of factors of N). To use CRT you might want to first turn N into something like N1 * N2 with N1, N2 coprime and then go from there (as I cant see a version of CRT that breaks ZMod into each prime factor, but I could just be looking in the wrong place)

[Thomas Lanard]

But if I use (N : ℕ+) then the rw doesn’t work

import Mathlib
open BigOperators

variable (N : ℕ+)

noncomputable instance : Fintype (GL (Fin n) (ZMod (N))) := Fintype.ofFinite (GL (Fin n) (ZMod N))

lemma card_GL_ZMod : Fintype.card (GL (Fin n) (ZMod (N.val))) =  1 := by
  have h : N.val ≠ 0 := PNat.ne_zero N
  have h2 : N.val = Finsupp.prod (Nat.factorization N.val) fun (x x_1 : ℕ) => x ^ x_1 := by rw [(Nat.factorization_prod_pow_eq_self h)]
  rw [h2]
  --tactic 'rewrite' failed, motive is not type correct

[Thomas Lanard]

Chris Birkbeck said:

Although I don't think it'll let you rewrite N in the Zmod N into Zmod (product of factors of N). To use CRT you might want to first turn N into something like N1 * N2 with N1, N2 coprime and then go from there (as I cant see a version of CRT that breaks ZMod into each prime factor, but I could just be looking in the wrong place)

We could use ZMod.prodEquivPi no?

[Chris Birkbeck]

Ah I missed that one! yes you are right, that would be what you want.

[Chris Birkbeck]

You can also try

variable (N : ℕ) [h : Fact (N ≠ 0)]

noncomputable instance : NeZero N := by exact { out := h.out }

instance : Fintype (ZMod (N)) := by
  have : NeZero N := by exact { out := h.out }
  apply ZMod.fintype N

noncomputable instance : Fintype (GL (Fin n) (ZMod (N))) := by
  have : NeZero N := by exact { out := h.out }
  apply Fintype.ofFinite (GL (Fin n) (ZMod N))

But I think this will also have the rw problem.

[Thomas Lanard]

Yes, same rw problem. Even for this, rw doesn’t work

lemma card_GL_ZMod (N: ℕ) (h : N ≠ 0) [Fintype (GL (Fin n) (ZMod N))]:
    Fintype.card (GL (Fin n) (ZMod (N))) =  1 := by
  rw [←(Nat.factorization_prod_pow_eq_self h)]
  --tactic 'rewrite' failed, motive is not type correct

[Chris Birkbeck]

hmm ok what about:

import Mathlib
open BigOperators

variable (N : ℕ)


instance : Fintype (ZMod (N + 1)) := by
  apply ZMod.fintype (N + 1)

noncomputable instance : Fintype (GL (Fin n) (ZMod (N+1))) := by

  apply Fintype.ofFinite (GL (Fin n) (ZMod (N+ 1)))

lemma card_GL_ZMod : Fintype.card (GL (Fin n) (ZMod (N+1))) =  1 := by
  --failed to synthesize instance Fintype (GL (Fin n) (ZMod N))
  --have := (Nat.factorization_prod_pow_eq_self h.out)
  apply Nat.recOnPosPrimePosCoprime (P := fun N => Fintype.card (GL (Fin n) (ZMod (N+1))) = 1)

[Chris Birkbeck]

this is quite ugly since it has N+1 everywhere, but the Nat.recOn cases you get might be doable

[Chris Birkbeck]

or perhaps, just replace the N+1 with N and use the NeZero stuff.

[Chris Birkbeck]

actually that probably wont work as itll factor N and not N+1

[Kevin Buzzard]

Why not use Finite instead of Fintype? That might solve the motive not being type correct error.

[Chris Birkbeck]

ah yes thats a good idea:

import Mathlib
open BigOperators

variable (N : ℕ) [h : Fact (N ≠ 0)]


instance : Fintype (ZMod (N )) := by
  haveI : NeZero (N) :=  by exact {out := h.out}
  refine ZMod.fintype N


noncomputable instance : Finite (GL (Fin n) (ZMod (N))) := by
 exact instFiniteUnits


lemma card_GL_ZMod : Nat.card (GL (Fin n) (ZMod (N))) =  1 := by
  --failed to synthesize instance Fintype (GL (Fin n) (ZMod N))
  have := (Nat.factorization_prod_pow_eq_self h.out)
  rw [← this]

[Chris Birkbeck]

That works

[Thomas Lanard]

Thank you! I will try with Nat.card then!

[Thomas Lanard]

It worked with Nat.card :smile:. Thank you!
I have pushed the proof in the repo (and also, as Riccardo wanted, the injectivity of $GL_n(A) \to GL_n(B)$ for an injective morphism $A \to B$, and surjectivity for a surjective local ring morphism).

[Chris Birkbeck]

Thats great! I'll try and have a look in the next few days. I guess the next thing is to think about cleaning it up to PR it to mathlib :)

[Chris Birkbeck]

"Next few days" was a lie, but I've just bumped the repo. Hopefully I'll have some time soonish to start PRing some of this.