\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Lie Theory in Mizar

Table of Contents

1. Overview

This is just a placeholder for my thinking about formalizing Lie algebras and Lie groups in Mizar. On the whole, it seems following Bourbaki's books may be the best outline/strategy.

2. Relevant Definitions

2.1. Existing in Mizar

Mizar's library is huge, here's what I could find at a glance that's relevant.

2.2. Not in Mizar

2.2.1. Differentiable Manifolds

It's kinda debatable whether this is needed, because topological groups are also Lie groups (Hilbert's fifth problem) thanks to a theorem by Andrew Gleason, Deane Montgomery, and Leo Zippin.

Most books define a Lie group as a real analytic manifold equipped with a smooth group structure (a few weaken this to just(!) a \(C^{\infty}\) manifold).

2.2.2. Lie Algebras

A vector space \(L\) over a field \(F\) with an operation \(L\times L\to L\), denoted \((x,y)\to[x, y]\) called the bracket (or commutator) of \(x\) and \(y\), is called a Lie Algbra over \(F\) if

  1. The bracket is bilinear
  2. \([x,x]=0\) for all \(x\in L\)
  3. \([x, [y,z]] + [y, [z,x]] + [z, [x,y]] = 0\) for all \(x,y,z\in L\).

This is the definition given by Humphreys' Introduction to Lie Algebras and Representation Theory (pg 1, third ed.). It is more narrow than the one Bourbaki gives in Lie Groups and Lie Algebras I.1§2 Definition 1:

An algebra \(\mathfrak{g}\) over a commutative unital [associative] ring \(K\) is called a Lie Algebra over \(K\) if its multiplication (denoted by \((x,y)\mapsto[x,y]\)) satisfies:

  1. \([x,x]=0\)
  2. \([x, [y,z]] + [y, [z,x]] + [z, [x,y]] = 0\)

for all \(x,y,z\in\mathfrak{g}\).

Bourbaki asserts that the Lie bracket is a bilinear alternating map, but it is not adequately justified. "Bilinear" yes, but "alternating"? No, not in general: only if the characteristic of \(K\) is not 2.

Mizar's notion of an algebra is almost good: they demand an algebra be unital, but this is not true in general for Lie algebras. Further, since multMagma is a distant ancestor of AlgebraStr, this means that an infixed * is provided for multiplication…which we don't want. Consequently, it seems that we should define a struct LieAlgebraStr which extends ModuleStr.

Unfortunately, Bilinear is defined as an attribute, but only for operators over real vector spaces. (See also Bilinear and BilinearOperator.) I think the definition can be generalized in a straightforward manner: just use additive and homogeneous (whereas we would want to use something like linear). Being homogeneous forces K to be a non empty multMagma (instead of just being 1-sorted). 

:: C.f., LOPBAN_8:5 and LOPBAN_8:6, FUNCT_5:def 1 and FUNCT_5:def 3
:: and RINGCAT1:def 1
definition
  let K be non empty multMagma;
  let L,M,N be ModuleStr over K
  let IT be Function of [:L,M:],N;
  attr IT is bilinear means
  (for l being Element of L st l in dom (curry IT)
   holds (curry IT).l is additive homogeneous Function of M,N) &
  (for m being Element of M st m in dom (curry' IT)
   holds (curry' IT).m is additive homogeneous Function of L,N);
end;

theorem Ex:
  for K being non empty multMagma
  for L,M,N being ModuleStr over K
  holds [: the carrier of L, the carrier of M :] --> (0.N) is bilinear;

registration
  let K be non empty multMagma;
  let L,M,N be ModuleStr over K;
  cluster bilinear for Function of [:L,M:],N;
  existence by Ex;
end;

registration
  let K be non empty multMagma;
  let M be ModuleStr over K;
  cluster bilinear for BinOp of M;
  existence by Ex;
end;

definition
  let K be non empty multMagma;
  struct (ModuleStr over K) LieAlgebraStr over K
  (# carrier -> set,
     addF -> BinOp of the carrier,
  bracket -> bilinear BinOp of the carrier,
    ZeroF -> Element of the carrier,
    lmult -> Function of [:the carrier of K,the carrier:], the carrier #);
end;

definition
  let K be non empty multMagma;
  let L be LieAlgebraStr over K;
  let x,y be Element of L;
  func [. x, y .] -> Element of L equals
  (the bracket of L).(x, y);
  coherence
  proof
    thus (the bracket of L).(x, y) is Element of L;
  end;
end;

definition
  let K be non empty multMagma;
  let IT be LieAlgebraStr over K;
  attr IT is LieAlgebra-like means :Def:
  (for x being Element of IT holds [. x, x .] = 0.IT)
  & (for x,y,z being Element of IT
     holds [. x, [. y, z .].] + [.y,[.z,x.].] + [.z,[.x,y.]] = 0.IT); 
end;

definition
  let K be non empty multMagma;
  mode LieAlgebra is LieAlgebra-like LieAlgebraStr over K;
  existence;
  :: ...
end;

:: RING_3:def 5 defines Char for a Ring
theorem
  for K being Ring st Char K <> 2
  for L being LieAlgebraStr over K
  for x,y being Element of L
  holds [. x,y .] = -1 * [. y,x .];

3. References

  • Oliver Nash,
    "Formalising Lie algebras".
    arXiv:2112.04570, 12 pages.
    • Discusses formalizing Lie algebras in Lean.
  • Meinolf Geck,
    "On the construction of semisimple Lie algebras and Chevalley groups".
    arXiv:1602.04583, 14 pages.
  • Jean-Pierre Serre,
    Complex semisimple Lie algebras.
    Springer, 1987.
  • Jim Humphreys,
    Definition of "finite group of Lie type"?
    Thread on Math.Overflow

Last Updated 2023-01-20 Fri 15:57.