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

m23_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: Existential: a finite 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. Both the MonoidAlgebra ℂ G action on V and on V ⊗[ℂ] V are bound explicitly, with IsScalarTower and an explicit diagonal-action equation g•(v⊗w) = (g•v)⊗(g•w) pinning the V⊗V action. The intended witness is M₂₃ acting on its 22-dim irreducible: V ⊗ V = 1 ⊕ V ⊕ W₂₃₀ ⊕ Λ²V. While the formal statement does not technically require constructing M₂₃ and studying its representation theory, we suspect that in practice it does.

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 ∧
      ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
        (_ : Module (MonoidAlgebra ℂ G) V)
        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) V)
        (_ : Module (MonoidAlgebra ℂ G) (V ⊗[ℂ] V))
        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)),
        Module.finrank ℂ V = 22 ∧
        IsSimpleModule (MonoidAlgebra ℂ G) V ∧
        (∀ (g : G) (v w : V),
          (MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • (v ⊗ₜ[ℂ] w) =
            ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • v) ⊗ₜ[ℂ]
              ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • w)) ∧
        (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4 := by⊢ ∃ G x x_1,
  Fintype.card G = 10200960 ∧
    ∃ V x_2 x_3 x_4,
      ∃ (x_5 : IsScalarTower ℂ (MonoidAlgebra ℂ G) V),
        ∃ x_6,
          ∃ (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)),
            Module.finrank ℂ V = 22 ∧
              IsSimpleModule (MonoidAlgebra ℂ G) V ∧
                (∀ (g : G) (v w : V),
                    (MonoidAlgebra.of ℂ G) g • v ⊗ₜ[ℂ] w =
                      ((MonoidAlgebra.of ℂ G) g • v) ⊗ₜ[ℂ] ((MonoidAlgebra.of ℂ G) g • w)) ∧
                  (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4
  sorryAll goals completed! 🐙

Solved by

Not yet solved.