Characters of finite groups

Complex characters and representations used to study finite groups: class functions and orthogonality, irreducible character bases, character degrees and values, McKay conjecture, rational groups, permutation characters, blocks of defect zero, Frobenius group determinant, convolution on finite groups, and Burnside's p^a q^b theorem; general representation theory of algebras and Lie groups belongs to RepresentationTheory.

• Blocks of defect zero
• Brauer's splitting field theorem
• Burnside's p^a q^b theorem
• Character degrees of Sylow subgroups
• Character degrees of symmetric groups
• Character values of simple groups
• Convolution on finite groups
• Frobenius group determinant
• Integer group determinants
• Irreducible characters and class functions
• McKay conjecture
• Permutation characters
• Rational groups
• Simply reducible groups

TheoremFour isotypic components in a tensor square for a simple group of order 10200960#●ready to prove

There exist a finite simple group \(G\) of order \(10200960\) and an irreducible complex representation \(\rho\) of \(G\) on a vector space \(V\) of dimension \(22\) such that the tensor square \(V \otimes V\), regarded as a module over the group algebra \(\mathbb{C}[G]\) through the diagonal action \(g \mapsto \rho(g) \otimes \rho(g)\), has exactly \(4\) isotypic components.

public theorem_wanted 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

Sources

• É. Mathieu, Sur les fonctions cinq fois transitives de 24 quantités, J. Math. Pures Appl. (1873); ATLAS of Finite Groups, M₂₃ character table. Problem m23_irrep_tensor_square_decomp of the lean-eval benchmark.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.