Existence of a simple group of order 10200960 with a 22-dim irrep whose tensor square has 4 isotypic components

m23_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: Existential: a finite SIMPLE group G of order 10200960 (= |M₂₃|) with a 22-dimensional irreducible complex representation V whose tensor square (with the diagonal G-action) has exactly 4 isotypic components. The diagonal action on V ⊗[ℂ] V is supplied explicitly via Module.compHom from ρ.tprod ρ. The intended witness is M₂₃ acting on its 22-dim irreducible: V ⊗ V = 1 ⊕ V ⊕ W₂₃₀ ⊕ Λ²V. Corrected 2026-06-27: the IsSimpleGroup G hypothesis was added after Lorenzo Luccioli (using Harmonic's Aristotle) solved an earlier order-only version with a solvable direct product G = SL(2,𝔽₃) × (C₂₃ ⋊ C₁₁) × C₁₆₈₀, exploiting multiplicativity of dimension and isotypic count under external tensor product. Simplicity excludes all decomposable witnesses; by CFSG the unique simple group of this order is M₂₃.

Source: É. Mathieu, Sur les fonctions cinq fois transitives de 24 quantités, J. Math. Pures Appl. (1873); ATLAS of Finite Groups, M₂₃ character table.

Informal solution: Realise M₂₃ as a subgroup of S₂₃ (e.g. via the Steiner system S(4,7,23) or as the automorphism group of a ternary Golay code construction). Take V to be the 22-dimensional deleted permutation representation. By 4-transitivity Sym²V is the permutation representation on the 23 choose 2 = 253 unordered pairs, decomposing as 1 + V + W₂₃₀ where W is the unique 230-dimensional irrep; Λ²V is irreducible of dimension 231, giving four pairwise non-isomorphic isotypic components in V⊗V.

theorem declaration uses `sorry`m23_irrep_tensor_square_decomp :
    ∃ (G : Type) (_ : Group G) (_ : Fintype G),
      Fintype.card G = 10200960 ∧
      IsSimpleGroup G ∧
      ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (ρ : Representation ℂ G V),
        Module.finrank ℂ V = 22 ∧
        ρ.IsIrreducible ∧
        (@isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V) _ _
          (Module.compHom (V ⊗[ℂ] V)
            (Representation.asAlgebraHom (ρ.tprod ρ)).toRingHom)).ncard = 4 := by⊢ ∃ G x x_1,
  Fintype.card G = 10200960 ∧
    IsSimpleGroup G ∧
      ∃ V x_2 x_3 ρ,
        Module.finrank ℂ V = 22 ∧ ρ.IsIrreducible ∧ (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4
  sorryAll goals completed! 🐙

Solved by

Not yet solved.