Existence of a 64-dim irreducible g₂-representation with 14 tensor-square isotypic components

g2_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: g₂ is the smallest exceptional Lie algebra, defined here by the Serre construction (Mathlib's `LieAlgebra.g₂`). The formal statement is existential: it asks for some 64-dimensional irreducible representation whose tensor square has 14 isotypic components. In the intended solution, one constructs such a witness using the highest-weight representation with highest weight ω₁ + ω₂ (the sum of the two fundamental weights). The U(g)-module structure on V ⊗ V used in the statement comes from lifting the Lie action via the universal enveloping algebra.

Source: Classical: representation theory of the exceptional Lie algebra g₂.

Informal solution: Construct V as the irreducible 64-dim representation V(ω₁+ω₂). Decomposition (LiE-verified): V⊗V = V(0,0) + V(1,0) + 2V(0,1) + 2V(2,0) + 2V(1,1) + 2V(0,2) + 3V(3,0) + 3V(2,1) + V(1,2) + V(0,3) + 2V(4,0) + 2V(3,1) + V(2,2) + V(5,0). This is used to produce the existential witness required by the formal statement.

theorem declaration uses `sorry`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 := by⊢ ∃ V x x_1 x_2,
  ∃ (x_3 : LieModule ℂ (LieAlgebra.g₂ ℂ) V),
    Module.finrank ℂ V = 64 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.g₂ ℂ) V ∧
        (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.g₂ ℂ)) (V ⊗[ℂ] V)).ncard = 14
  sorryAll goals completed! 🐙

Solved by

Not yet solved.