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)