lie algebra

Stream: Is there code for X?

[Edison Xie]

I'm trying to revise for my final exam, I got curious and want to formalise some of my past paper question in lean but I couldn't find $\mathfrak{sl}_n$, $\mathfrak{o}_n$ or $\mathfrak{t}_n$, does anyone know where they are?

[Oliver Nash]

We have docs#LieAlgebra.SpecialLinear.sl and docs#LieAlgebra.Orthogonal.so but they were added a long time ago (when we were all less experienced) and haven't been touched since, so I wouldn't be surprised if they could do with some attention.

[Oliver Nash]

Indeed glancing over the file in which these are defined, I note that the naming (due to me) is quite poor.

[Edison Xie]

Oliver Nash said:

We have docs#LieAlgebra.SpecialLinear.sl and docs#LieAlgebra.Orthogonal.so

do we have the dimension of them as well?

[Kevin Buzzard]

Sounds like a great exercise :-)

[Edison Xie]

Kevin Buzzard said:

Sounds like a great exercise :-)

already proved them :-) using my own crappy definition of $\mathfrak{sl}_n$ though

[Edison Xie]

looks like we have docs#LieAlgebra.SpecialLinear.Eb but we don't have {$E_{ij} \mid i \ne j$} $\cup$ {$E_{ii} - E_{(i+1)(i+1)}$} forms a basis of $\mathfrak{sl}_n$

[Edison Xie]

Also why does

import Mathlib
variable (n R : Type*) [Fintype n] [DecidableEq n] [CommRing R]

open LieAlgebra
lemma mem_sl_iff (A : Matrix n n R): A ∈ SpecialLinear.sl n R ↔ A.trace = 0 := by rfl

works but

lemma mem_sl_iff (A : Matrix n n R): A ∈ SpecialLinear.sl n R ↔ A.trace = 0 := rfl

does not work?

[Kevin Buzzard]

Term mode rfl only works on equality. Tactic rfl is more flexible.

[Eric Wieser]

Iff.rfl should work

[Edison Xie]

It does work!

[Edison Xie]

import Mathlib

variable {R : Type*} [CommRing R]
open LieAlgebra

section

variable {n : Type*} [Fintype n] [DecidableEq n]
@[simp]
lemma mem_sl_iff (A : Matrix n n R): A ∈ SpecialLinear.sl n R ↔ A.trace = 0 := Iff.rfl

end

variable {R : Type*} [CommRing R] {n : ℕ}

lemma divn_mem1 (i : Fin (n*n - 1)) : i/n < n := by
  obtain ⟨i, hi⟩ := i
  simpa using Nat.div_lt_of_lt_mul <| Nat.lt_trans hi (by omega)

lemma modn_mem1 (i : Fin (n*n - 1)) [NeZero n] : i%n < n := by
  obtain ⟨i, hi⟩ := i
  simpa using Nat.mod_lt i <| Nat.pos_of_neZero n

abbrev LieAlgebra.SpecialLinear.Eb' (i : Fin n) (hi : i < n - 1):
    LieAlgebra.SpecialLinear.sl (Fin n) R :=
  ⟨Matrix.stdBasisMatrix i i 1 - Matrix.stdBasisMatrix ⟨i + 1, Nat.add_lt_of_lt_sub hi⟩
    ⟨i + 1, Nat.add_lt_of_lt_sub hi⟩ 1, by simp⟩

lemma modn_mem2 (i : Fin (n*n - 1)) [NeZero n] (h : i%n = i/n) : i%n < n - 1 := by
  have := modn_mem1 i
  obtain ⟨i, hi⟩ := i
  simp at *
  suffices i%n ≠ n - 1 by omega
  intro hh
  have : i = i%n + (i/n) * n := (Nat.mod_add_div' i n).symm
  rw [h, hh] at *
  rw [Nat.sub_mul, one_mul, add_comm, ← Nat.add_sub_assoc (by omega),
    Nat.sub_add_cancel (by omega)] at this
  omega

abbrev sln_basisAux [NeZero n]: Fin (n*n - 1) → SpecialLinear.sl (Fin n) R := fun i ↦
  if h : i/n ≠ i%n then SpecialLinear.Eb _ ⟨i/n, divn_mem1 i⟩ ⟨i%n, modn_mem1 i⟩
    (Fin.ne_of_val_ne (Ne.symm h))
  else SpecialLinear.Eb' ⟨i%n, modn_mem1 i⟩ <| modn_mem2 i (by tauto)

This should be the right basis?(I just adapted mathlib's code) @Oliver Nash @Kevin Buzzard

[Eric Wieser]

Is Fin (n*n -1) really the most natural indexing type?

[Edison Xie]

it's definitely not but I don't know if there's a better substitution

[Edison Xie]

Fin (n + 1) times Fin (n - 1) is even worse

[Eric Wieser]

I would guess you want { x : m × m // x.1 ≠ x.2 } \o+ {y // y ≠ y0}

[Edison Xie]

what is y0?

[Eric Wieser]

An argument to your function producing a basis

[Eric Wieser]

(For Fin you could pick 0, but for a more general index type you should let the caller pick)

[Edison Xie]

Eric Wieser said:

(For Fin you could pick 0, but for a more general index type you should let the caller pick)

so it's {y : Fin n // y ≠ ⟨0, sorry⟩}?

[Eric Wieser]

No, you should literally write what I did above (modulo Unicode), don't mention Fin

[Andrew Yang]

I guess it is hard to talk about the basis of the diagonal elements without breaking some symmetry.
Maybe just do Finset.univ (α := Fin (n + 1)).offDiag ⊕ Fin n

[Eric Wieser]

It should be the callers job to decide how to break symmetry

[Andrew Yang]

So you want to provide two injections n -> m that covers m instead to replace Fin.succ and Fin.castSucc?

[Eric Wieser]

Why do you need succ and castSucc?

[Andrew Yang]

Oh I see what you mean now. I was stuck on how Edison defined Eb'.

[Eric Wieser]

Just use $\{E_{ij} \mid i \ne j\} \cup \{E_{ii} - E_{i_0,i_0}\}$ as the basis instead

[Kevin Buzzard]

It's always difficult picking a basis for vector spaces like $\{(x,y,z)\in\R^3\mid x+y+z=0\}$ because you have to break the symmetry

[Kevin Buzzard]

Why do we need a basis anyway?

[Edison Xie]

Kevin Buzzard said:

Why do we need a basis anyway?

I want to prove dim sln = n^2 - 1

[Kevin Buzzard]

Then use rank nullity

[Kevin Buzzard]

The dimension of that space I said above is 2 because it's 3-1

[Edison Xie]

so the basis is useless for us? (I mean, not just for the dimension problem)

[Kevin Buzzard]

Sometimes you have to pick a basis to do a calculation but if all you want is the dimension then maybe rank nullity is an easier approach?

[Kevin Buzzard]

Later on in the theory you need to choose fundamental roots and the like, but by that point you've chosen an ordering on the basis of V so you've broken the symmetry anyway

[Edison Xie]

yeah massive calculation looks inevitable

[Eric Wieser]

We should build the basis anyway, because it's the easiest path to showing it's a free module

[Eric Wieser]

Something like:

noncomputable def basis (i₀ : n) : Basis ({ x : n × n // x.1 ≠ x.2 } ⊕ {y // y ≠ i₀}) R (SpecialLinear.sl n R) :=
  .ofEquivFun <| {
    toFun M := (fun ij : { x : n × n // x.1 ≠ x.2 } => M.val ij.1.1 ij.1.2, fun i : {y // y ≠ i₀} => M.val i i - M.val i₀ i₀)
    map_add' _ _ := by ext <;> dsimp <;> simp [sub_add_sub_comm]
    map_smul' _ _ := by ext <;> dsimp <;> erw [Submodule.coe_smul] <;> simp [mul_sub] <;> rfl
    invFun c := ∑ ij, c.1 ij • SpecialLinear.Eb R _ _ ij.prop + ∑ i, c.2 i • SpecialLinear.Eb' R _ _
    left_inv _ := sorry
    right_inv _ := sorry
  } ≪≫ₗ (LinearEquiv.sumArrowLequivProdArrow _ _ R R |>.symm)

[Eric Wieser]

Probably we should redefine Eb to take an extra r : R argument to match stdBasisMatrix

[Edison Xie]

if we require Inhabited n is that gonna work? because dimension of $sl_0$ is 0 instead of -1

[Eric Wieser]

Which "that" are you referring to?

[Edison Xie]

I mean we just add an assumption to n forcing it to have a default element then i0 is the default element

[Eric Wieser]

I don't think that's better than making the caller choose

[Edison Xie]

why do you think that's the case?

[Eric Wieser]

For the same reason we have docs#List.getD and not just docs#List.getI

[Eric Wieser]

At any rate, I would expect there to be very few callers

[Eric Wieser]

In the Module.Free instance, you'd case split on empty or non empty, and use cases to pick an arbitrary element

[Edison Xie]

how do I work with summing over { x : n × n // x.1 ≠ x.2 }? i.e

lemma finalstep {R n: Type*} [CommRing R] [Fintype n] [DecidableEq n] (M : Matrix n n R)
    (hM : M ∈ SpecialLinear.sl n R) (i j : n) (hij : i ≠ j) :
    (∑ x : {x : n × n // x.1 ≠ x.2}, if x.1.2 = i ∧ x.1.1 = j
    then M x.1.1 x.1.2 else 0) = M i j := by
  sorry

this should be easy right? @Eric Wieser

[Eric Wieser]

docs#Finset.sum_subtype ? (edit: not quite)

[Eric Wieser]

docs#Fintype.sum_eq_single

[Edison Xie]

docs#Fintype.sum_eq_single requires an element in { x : n × n // x.1 ≠ x.2 } but do we have that element?

[Eric Wieser]

Yes, it's \<(i, j), hij\>

[Edison Xie]

I somehow end up with the goal M i j = 0 I don't think this goal is provable?

[Edison Xie]

lemma finalstep {R n: Type*} [CommRing R] [Fintype n] [DecidableEq n](i₀ : n) (M : Matrix n n R)
    (hM : M ∈ SpecialLinear.sl n R) (i j : n) (hij : i ≠ j) :
    (∑ x : {x : n × n // x.1 ≠ x.2}, if x.1.2 = i ∧ x.1.1 = j
    then M x.1.1 x.1.2 else 0) = M i j := by
  rw [Fintype.sum_eq_single ⟨⟨i, j⟩, hij⟩ (by
    simp;
    intro a b h1 h2 h3 h4; sorry)]
  simp [hij]

  sorry

[Edward van de Meent]

ah yes, the condition you wrote in the if is x.1 = (j,i)

[Edward van de Meent]

which seems backwards

[Edward van de Meent]

are you sure this is the correct formalization of your theorem?

[Edison Xie]

Edward van de Meent said:

ah yes, the condition you wrote in the if is x.1 = (j,i)

yes changing it back does work but this is an extraction from my proof to eric's remaining sorrys...

[Edward van de Meent]

i guess that must mean that you swapped the indices around somewhere

[Edison Xie]

yeah I'm trying to spot where to swap

[Edison Xie]

okay it worked thanks!

[Edison Xie]

Eric Wieser said:

M.val ij.1.1 ij.1.2

I should swap this

[Eric Wieser]

Is docs#LieAlgebra.SpecialLinear.Eb backwards? (edit: no)

[Eric Wieser]

I don't see why you would need to swap it

[Edison Xie]

I don't think so, the solution to my problem is to swap the line I mentioned above as well as changing <i, j> to <j, i>

[Eric Wieser]

What's your full proof so far?

[Edison Xie]

import Mathlib

variable {R : Type*} [CommRing R]
open LieAlgebra

noncomputable section

variable {n : Type*} [Fintype n] [DecidableEq n]
@[simp]
lemma mem_sl_iff (A : Matrix n n R): A ∈ SpecialLinear.sl n R ↔ A.trace = 0 := Iff.rfl

abbrev LieAlgebra.SpecialLinear.Eb' (i : n) (i₀ : n):
    LieAlgebra.SpecialLinear.sl n R :=
  ⟨Matrix.stdBasisMatrix i i 1 - Matrix.stdBasisMatrix i₀ i₀ 1, by simp⟩

omit [Fintype n] in
@[simp]
lemma Matrix.StdBasisMatrix.of_ne (c i j : n) (hij : i ≠ j) (r : R):
    Matrix.stdBasisMatrix c c (r : R) i j = 0 := by
  aesop

def basis (i₀ : n) : Basis ({ x : n × n // x.1 ≠ x.2 } ⊕ {y // y ≠ i₀}) R (SpecialLinear.sl n R) :=
  .ofEquivFun <| {
    toFun M := (fun ij : { x : n × n // x.1 ≠ x.2 } => M.val ij.1.2 ij.1.1,
      fun i : {y // y ≠ i₀} => M.val i i - M.val i₀ i₀)
    map_add' _ _ := by ext <;> dsimp; simp [sub_add_sub_comm]
    map_smul' _ _ := by ext <;> dsimp <;> rw [Submodule.coe_smul] <;> simp [mul_sub]
    invFun c := ∑ ij, c.1 ij • SpecialLinear.Eb R _ _ ij.prop + ∑ i, c.2 i •
      SpecialLinear.Eb' i.1 i₀
    left_inv x := by
      obtain ⟨M, hM⟩ := x
      simp [Subtype.ext_iff]
      ext i j
      simp [Matrix.sum_apply, SpecialLinear.Eb, SpecialLinear.Eb']
      conv => enter[1, 2, 2]; change fun c ↦ (M c.1 c.1 - M i₀ i₀) • (_ - _)
      if hij : i ≠ j then
      simp [show Matrix.stdBasisMatrix i₀ i₀ (1 : R) i j = 0 from
        Matrix.StdBasisMatrix.of_ne i₀ i j hij 1]
      conv => enter[1, 2]; rw [show ∑ x : { y // y ≠ i₀ }, (M x x - M i₀ i₀) *
        Matrix.stdBasisMatrix x.1 x.1 1 i j = 0 from Finset.sum_eq_zero fun i' _ ↦ by
        rw [Matrix.StdBasisMatrix.of_ne i'.1 i j hij (1 : R), mul_zero]]
      simp [Matrix.stdBasisMatrix]
      rw [Fintype.sum_eq_single ⟨⟨j, i⟩, Ne.symm hij⟩ (by simp; tauto)]
      simp [hij] else
      simp at hij
      subst hij

      sorry
    right_inv _ := sorry
  } ≪≫ₗ (LinearEquiv.sumArrowLequivProdArrow _ _ R R |>.symm)

end

[Eric Wieser]

SpecialLinear.Eb is indeed backwards

[Eric Wieser]

Using SpecialLinear.Eb R i j ij.prop.symm fixes it

[Eric Wieser]

But the symm shouldn't be there ,Eb should take its arguments in order

[Edison Xie]

Eric Wieser said:

SpecialLinear.Eb is indeed backwards

should we open a PR to fix that?

[Eric Wieser]

Yes, and you may as well add Eb' in the same one

[Edison Xie]

will do (after exam), or if anyone needs it feel free to do it :)

[Eric Wieser]

#24613 does just the flip, and adding an r argument

[Eric Wieser]

I refrained from adding Eb', since #mathlib4 > Renaming docs#Matrix.stdBasisMatrix @ 💬 might mean we want to name it something else

[Eric Wieser]

#24645 adds Eb', with name singleSubSingle