Center of General Linear Group

Stream: maths

[Alex Brodbelt]

I'm working on proving that the center of GL(n, R) is the set of scalar matrices with unit entries as I will need this later on.

I just saw another thread mention how one should go about working on contributions, so I thought I would ask for feedback about definitions and theorems I am trying to prove to eventually get to this result.

I have started of defining the transvection matrices and shown they belong to SpecialLinearGroup n R to then show they belong to GL n R ( a quick suggestion from @Eric Wieser) - (I was also wondering if it would be worth modifying the notation to be SL n R (similar to how it is for GL n R ) currently the notation is SL(n, R) and is associated to Matrix.SpecialLinearGroup (Fin n) R.

I also made definitions to coerce TransvectionStruct into SL and GL, they are trivial but I wonder if for completeness they should be they should be in Mathlib/LinearAlgebra/Matrix/Transvection.lean.

Similarly, I define the scalar matrices for the general linear group where the entries are the units of the ring.

For the theorem at the end, I am having trouble modifying mem_range_scalar_of_commute_transvectionStruct to take in matrices from GL n R, there are currently two approaches in my head:

• try use mem_range_scalar_of_commute_transvectionStruct and then prove that if M : GL n R and (M : Matrix n n R) ∈ Set.range (Matrix.scalar n) then ∃ r : Rˣ, GeneralLinearGroup.scalar n R r r.isUnit = M (the definition for this scalar matrix is below)
• Alternatively, I am thinking of proving this result ∃ r : Rˣ, GeneralLinearGroup.scalar n R r r.isUnit = M directly whether it be through using a modifiedSet.range

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
import Mathlib.LinearAlgebra.Matrix.Transvection

namespace Matrix

universe u v

open Matrix

open scoped MatrixGroups

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

variable (i j : n) (c : R)

namespace SpecialLinearGroup
-- maybe improve notation
def transvection (hij : i ≠ j) : SpecialLinearGroup n R :=
  ⟨Matrix.transvection i j c, (det_transvection_of_ne i j hij (c : R))⟩

end SpecialLinearGroup

namespace TransvectionStruct

def toSL (t : TransvectionStruct n R) : SpecialLinearGroup n R := ⟨t.toMatrix, by simp⟩


def toGL (t : TransvectionStruct n R) : GL n R := t.toSL

end TransvectionStruct

namespace GeneralLinearGroup

def transvection (hij : i ≠ j) : GL n R :=
  (SpecialLinearGroup.transvection n R i j c hij).coeToGL

--does it necessarily have to be noncomputable? or is it just because I don't know how to use `GeneralLinearGroup.mk'`
noncomputable def scalar (r : R) (hr : IsUnit r) : GL n R :=
  GeneralLinearGroup.mk'' (Matrix.scalar n r)
  (by simp; apply IsUnit.pow _ hr)

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

#check mem_range_scalar_of_commute_transvectionStruct

/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). -/
theorem mem_range_unit_scalar_of_commute_transvectionStruct {M : GL n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toGL M):
    -- instead of `M ∈ Set.range (Matrix.scalar n), I wrote
    (M : Matrix n n R) ∈ Set.range (Matrix.scalar n) := by
  -- I'm not sure how to restrict the range to the units or if this would be more useful
  refine @mem_range_scalar_of_commute_stdBasisMatrix n R _ _ _ (M : Matrix n n R) ?h
  intro i j hij
  simpa [transvection, mul_add, add_mul] using (hM ⟨i, j, hij, 1⟩).eq --nearly works but struggles with breaking down my new definitions.

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ˣ, M = scalar n R r r.isUnit) := 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₁ : ∃ r : Rˣ, (GeneralLinearGroup.scalar n R r r.isUnit = M) := sorry--mem_range_unit_scalar_of_commute_transvectionStruct n R h₀
    obtain ⟨r, rfl⟩ := h₁
    use r
  · sorry --omitted

end GeneralLinearGroup

end Matrix

Thanks in advance!

Also please move this to new members if you think it is more suitable there.

[Johan Commelin]

@Corentin Cornou I think you had a result in this direction in your project, right?

[Eric Wieser]

What is GeneralLinearGroup.mk'' there?

[Eric Wieser]

Regarding your comment about noncomputability, this resolves it:

def scalar (r : Rˣ) : GL n R :=
  Units.map (Matrix.scalar n).toMonoidHom r

[Alex Brodbelt]

Eric Wieser said:

What is GeneralLinearGroup.mk'' there?

This is the definition in mathlib

/-- Given a matrix with unit determinant we get an element of `GL n R`-/
noncomputable def mk'' (A : Matrix n n R) (h : IsUnit (Matrix.det A)) : GL n R :=
  nonsingInvUnit A h

[Eric Wieser]

Ah, docs#Matrix.GeneralLinearGroup.mk''. Your #mwe seems to be missing some open/variable lines, so doesn't work as written

[Alex Brodbelt]

Eric Wieser said:

Ah, docs#Matrix.GeneralLinearGroup.mk''. Your #mwe seems to be missing some open/variable lines, so doesn't work as written

sorry - just updated it

[Eric Wieser]

Here's one lemma you struggled with:

/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). -/
theorem mem_range_unit_scalar_of_commute_transvectionStruct {M : GL n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toGL M):
    -- instead of `M ∈ Set.range (Matrix.scalar n), I wrote
    (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

[Patrick Massot]

Are you really really sure you want matrices here? The result holds in infinite dimension and the abstract proof is simpler.

[Alex Brodbelt]

Patrick Massot said:

Are you really really sure you want matrices here? The result holds in infinite dimension and the abstract proof is simpler.

Matrices are what are most familiar to me, but I'd be keen to see what you mean?

I would appreciate if you could start me off

...I believe I was mainly following the example of what was done with the Special Linear Group and determining its center

[Patrick Massot]

Let $V$ be a vector space over any field (with any dimension, possibly infinite). Let $φ$ be an invertible endomorphism of $V$. Assume the $φ$ commutes with every invertible endomorphism. You want to prove $φ$ is a multiple of identity. The first thing to prove is that, for every vector $x$ of $V$ , there is some $μ$ in the base field such that $φx = μx$. Then it remains to prove that all vectors share the same $μ$.

[Eric Wieser]

We now have a docs#Algebra.IsCentral to state this with, right?

[Alex Brodbelt]

Great, I'll have a look at this! Thank you