Products of bases Lie algebras #
Given two finite-dimensional simple Lie algebras, if they admit bases with matching Cartan matrices,
they must be isomorphic. This file provides a proof of this as LieAlgebra.Basis.equivOfReindex.
noncomputable def
LieAlgebra.Basis.equivOfReindex
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{L₁ : Type u_3}
{L₂ : Type u_4}
[Finite ι₁]
[Finite ι₂]
(eι : ι₁ ≃ ι₂)
[LieRing L₁]
[LieRing L₂]
{K : Type u_5}
[Field K]
[CharZero K]
[LieAlgebra K L₁]
[FiniteDimensional K L₁]
{H₁ : LieSubalgebra K L₁}
(b₁ : Basis ι₁ H₁)
[LieAlgebra K L₂]
[FiniteDimensional K L₂]
{H₂ : LieSubalgebra K L₂}
(b₂ : Basis ι₂ H₂)
(hA : (Matrix.reindex eι eι) b₁.A = b₂.A)
[IsSimple K L₁]
[IsSimple K L₂]
:
Simple Lie algebras with equivalent bases are equivalent.
Equations
- LieAlgebra.Basis.equivOfReindex eι b₁ b₂ hA = (LieAlgebra.Basis.prodEquivLeft✝ eι b₁ b₂ hA).symm.trans (LieAlgebra.Basis.prodEquivRight✝ eι b₁ b₂ hA)