feat(algebra/lie/cartan_matrix): define the exceptional Lie algebras (#…

…8299)

docs/references.bib

@@ -181,6 +181,20 @@ @Book{            bourbaki1975
   mrnumber      = {1728312}
 }
 
+@Book{            bourbaki1968,
+  author        = {Bourbaki, Nicolas},
+  title         = {Lie groups and {L}ie algebras. {C}hapters 4--6},
+  series        = {Elements of Mathematics (Berlin)},
+  note          = {Translated from the 1968 French original by Andrew
+                   Pressley},
+  publisher     = {Springer-Verlag, Berlin},
+  year          = {2002},
+  pages         = {xii+300},
+  isbn          = {3-540-42650-7},
+  mrclass       = {17-01 (00A05 20E42 20F55 22-01)},
+  mrnumber      = {1890629}
+}
+
 @Book{            bourbaki1975b,
   author        = {Bourbaki, Nicolas},
   title         = {Lie groups and {L}ie algebras. {C}hapters 7--9},

src/algebra/lie/cartan_matrix.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import algebra.lie.free
 import algebra.lie.quotient
+import data.matrix.notation
 
 /-!
 # Lie algebras from Cartan matrices
@@ -42,15 +43,35 @@ However the difference is illusory since the construction stays inside the Lie s
 `free_algebra R X` generated by `X`, and this is naturally isomorphic to `free_lie_algebra R X`
 (though the proof of this seems to require Poincaré–Birkhoff–Witt).
 
+## Definitions of exceptional Lie algebras
+
+This file also contains the Cartan matrices of the exceptional Lie algebras. By using these in the
+above construction, it thus provides definitions of the exceptional Lie algebras. These definitions
+make sense over any commutative ring. When the ring is ℝ, these are the split real forms of the
+exceptional semisimple Lie algebras.
+
 ## References
 
+* [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 4--6*](bourbaki1968) plates V -- IX,
+  pages 275--290
+
 * [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 7--9*](bourbaki1975b) chapter VIII, §4.3
 
 * [J.P. Serre, *Complex Semisimple Lie Algebras*](serre1965) chapter VI, appendix
 
 ## Main definitions
 
   * `matrix.to_lie_algebra`
+  * `cartan_matrix.E₆`
+  * `cartan_matrix.E₇`
+  * `cartan_matrix.E₈`
+  * `cartan_matrix.F₄`
+  * `cartan_matrix.G₂`
+  * `lie_algebra.e₆`
+  * `lie_algebra.e₇`
+  * `lie_algebra.e₈`
+  * `lie_algebra.f₄`
+  * `lie_algebra.g₂`
 
 ## Tags
 
@@ -147,7 +168,102 @@ end cartan_matrix
 
 Note that it is defined for any matrix of integers. Its value for non-Cartan matrices should be
 regarded as junk. -/
-@[derive [lie_ring, lie_algebra R]]
+@[derive [inhabited, lie_ring, lie_algebra R]]
 def matrix.to_lie_algebra := (cartan_matrix.relations.to_ideal R A).quotient
 
-instance (A : matrix B B ℤ) : inhabited (matrix.to_lie_algebra R A) := ⟨0⟩
+namespace cartan_matrix
+
+/-- The Cartan matrix of type e₆. See [bourbaki1968] plate V, page 277.
+
+The corresponding Dynkin diagram is:
+```
+            o
+            |
+o --- o --- o --- o --- o
+```
+-/
+def E₆ : matrix (fin 6) (fin 6) ℤ := ![![ 2,  0, -1,  0,  0,  0],
+                                       ![ 0,  2,  0, -1,  0,  0],
+                                       ![-1,  0,  2, -1,  0,  0],
+                                       ![ 0, -1, -1,  2, -1,  0],
+                                       ![ 0,  0,  0, -1,  2, -1],
+                                       ![ 0,  0,  0,  0, -1,  2]]
+
+/-- The Cartan matrix of type e₇. See [bourbaki1968] plate VI, page 281.
+
+The corresponding Dynkin diagram is:
+```
+            o
+            |
+o --- o --- o --- o --- o --- o
+```
+-/
+def E₇ : matrix (fin 7) (fin 7) ℤ := ![![ 2,  0, -1,  0,  0,  0,  0],
+                                       ![ 0,  2,  0, -1,  0,  0,  0],
+                                       ![-1,  0,  2, -1,  0,  0,  0],
+                                       ![ 0, -1, -1,  2, -1,  0,  0],
+                                       ![ 0,  0,  0, -1,  2, -1,  0],
+                                       ![ 0,  0,  0,  0, -1,  2, -1],
+                                       ![ 0,  0,  0,  0,  0, -1,  2]]
+
+/-- The Cartan matrix of type e₈. See [bourbaki1968] plate VII, page 285.
+
+The corresponding Dynkin diagram is:
+```
+            o
+            |
+o --- o --- o --- o --- o --- o --- o
+```
+-/
+def E₈ : matrix (fin 8) (fin 8) ℤ := ![![ 2,  0, -1,  0,  0,  0,  0,  0],
+                                       ![ 0,  2,  0, -1,  0,  0,  0,  0],
+                                       ![-1,  0,  2, -1,  0,  0,  0,  0],
+                                       ![ 0, -1, -1,  2, -1,  0,  0,  0],
+                                       ![ 0,  0,  0, -1,  2, -1,  0,  0],
+                                       ![ 0,  0,  0,  0, -1,  2, -1,  0],
+                                       ![ 0,  0,  0,  0,  0, -1,  2, -1],
+                                       ![ 0,  0,  0,  0,  0,  0, -1,  2]]
+
+/-- The Cartan matrix of type f₄. See [bourbaki1968] plate VIII, page 288.
+
+The corresponding Dynkin diagram is:
+```
+o --- o =>= o --- o
+```
+-/
+def F₄ : matrix (fin 4) (fin 4) ℤ := ![![ 2, -1,  0,  0],
+                                       ![-1,  2, -2,  0],
+                                       ![ 0, -1,  2, -1],
+                                       ![ 0,  0, -1,  2]]
+
+/-- The Cartan matrix of type g₂. See [bourbaki1968] plate IX, page 290.
+
+The corresponding Dynkin diagram is:
+```
+o ≡>≡ o
+```
+Actually we are using the transpose of Bourbaki's matrix. This is to make this matrix consistent
+with `cartan_matrix.F₄`, in the sense that all non-zero values below the diagonal are -1. -/
+def G₂ : matrix (fin 2) (fin 2) ℤ := ![![ 2, -3],
+                                       ![-1,  2]]
+
+end cartan_matrix
+
+namespace lie_algebra
+
+/-- The exceptional split Lie algebra of type e₆. -/
+abbreviation e₆ := cartan_matrix.E₆.to_lie_algebra R
+
+/-- The exceptional split Lie algebra of type e₇. -/
+abbreviation e₇ := cartan_matrix.E₇.to_lie_algebra R
+
+/-- The exceptional split Lie algebra of type e₈. -/
+abbreviation e₈ := cartan_matrix.E₈.to_lie_algebra R
+
+/-- The exceptional split Lie algebra of type f₄. -/
+abbreviation f₄ := cartan_matrix.F₄.to_lie_algebra R
+
+/-- The exceptional split Lie algebra of type g₂. -/
+abbreviation g₂ := cartan_matrix.G₂.to_lie_algebra R
+
+end lie_algebra