Tensor squares of exceptional Lie algebra representations

TheoremTensor square of an irreducible \(\mathfrak{g}_2\)-representation of dimension \(64\)#●ready to prove

There exist a complex vector space \(V\) and a representation of the exceptional Lie algebra \(\mathfrak{g}_2\) over \(\mathbb{C}\) on \(V\) such that \(V\) has dimension \(64\) over \(\mathbb{C}\), \(V\) is irreducible, and the tensor square \(V \otimes_{\mathbb{C}} V\), with the representation \(x \cdot (v \otimes w) = (x \cdot v) \otimes w + v \otimes (x \cdot w)\) viewed as a module over the universal enveloping algebra of \(\mathfrak{g}_2\), has exactly \(14\) isotypic components.

public theorem_wanted g2_irrep_tensor_square_decomp :
    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
      (_ : LieRingModule (LieAlgebra.g₂ ℂ) V) (_ : LieModule ℂ (LieAlgebra.g₂ ℂ) V),
      Module.finrank ℂ V = 64 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.g₂ ℂ) V ∧
      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.g₂ ℂ))
        (V ⊗[ℂ] V)).ncard = 14

Sources

• Classical: representation theory of the exceptional Lie algebra g₂. Problem g2_irrep_tensor_square_decomp of the lean-eval benchmark.

TheoremTensor square of an irreducible \(\mathfrak{e}_8\)-representation of dimension \(779247\)#●ready to prove

There exist a complex vector space \(V\) and a representation of the exceptional Lie algebra \(\mathfrak{e}_8\) over \(\mathbb{C}\) on \(V\) such that \(V\) has dimension \(779247\) over \(\mathbb{C}\), \(V\) is irreducible, and the tensor square \(V \otimes_{\mathbb{C}} V\), with the representation \(x \cdot (v \otimes w) = (x \cdot v) \otimes w + v \otimes (x \cdot w)\) viewed as a module over the universal enveloping algebra of \(\mathfrak{e}_8\), has exactly \(40\) isotypic components.

public theorem_wanted e8_irrep_tensor_square_decomp :
    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
      (_ : LieRingModule (LieAlgebra.e₈ ℂ) V) (_ : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
      Module.finrank ℂ V = 779247 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ))
        (V ⊗[ℂ] V)).ncard = 40

Sources

• Classical: representation theory of the exceptional Lie algebra e₈. Problem e8_irrep_tensor_square_decomp of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.