Burnside's p^a q^b theorem

TheoremIrreducible representations are simple#✓fully proved

Let \(G\) be a finite group and \(\sigma\) an irreducible representation of \(G\) on a finite-dimensional complex vector space \(V\). Then \(V\) with the action \(\sigma\) is a simple object of the category of finite-dimensional complex representations of \(G\).

theorem simple_fdrep_of_irreducible {V : Type} [AddCommGroup V] [Module ℂ V]
    [Module.Finite ℂ V] [Finite G] (σ : Representation ℂ G V) [σ.IsIrreducible] :
    Simple (FDRep.of σ)
Used by 2
Used byClass functions orthogonal to all irreducible characters vanish · The trivial irreducible class

TheoremSimple finite-dimensional representations are irreducible (auxiliary form)#✓fully proved

Let \(G\) be a finite group and \(V\) a simple object of the category of finite-dimensional complex representations of \(G\). If \(\sigma\) is a representation of \(G\) on the underlying vector space of \(V\) that equals the action of \(G\) on \(V\), then \(\sigma\) is irreducible.

theorem irreducible_of_simple_fdrep_aux (V : FDRep ℂ G) [Simple V] [Finite G]
    (σ : Representation ℂ G V)
    (hσ : (V.ρ : Representation ℂ G V) = σ) :
    σ.IsIrreducible
Used by 1
Used bySimple finite-dimensional complex representations of a finite group are irreducible

TheoremSimple finite-dimensional complex representations of a finite group are irreducible#✓fully proved

Let \(G\) be a finite group. If \(V\) is a simple object of the category of finite-dimensional complex representations of \(G\), then the representation of \(G\) on the underlying vector space of \(V\) is irreducible.

theorem irreducible_of_simple_fdrep (V : FDRep ℂ G) [Simple V] [Finite G] :
    Representation.IsIrreducible (V.ρ : Representation ℂ G V)
Uses 1 · Used by 1
Proof usesSimple finite-dimensional representations are irreducible (auxiliary form)
Used byA simple group with a prime-power conjugacy class has prime order

DefinitionIsomorphism of simple representations#✓fully proved

For a finite group \(G\), two simple finite-dimensional complex representations of \(G\) are related when they are isomorphic; this is an equivalence relation on the simple finite-dimensional complex representations of \(G\).

def Simple.isoSetoid : Setoid {V : FDRep ℂ G // Simple V} where
  r S T := Nonempty (S.1 ≅ T.1)
  iseqv := ⟨fun _ => ⟨Iso.refl _⟩, fun h => h.elim fun i => ⟨i.symm⟩,
    fun h1 h2 => h1.elim fun i => h2.elim fun j => ⟨i.trans j⟩⟩
Used by 10
Used byCharacter of an isomorphism class · Character of a class via its chosen representative · Characters determine irreducible representations · Character value at the identity · Orthogonality of irreducible characters · Class functions orthogonal to all irreducible characters vanish · Expansion of class functions in irreducible characters · Isomorphism classes of simple representations · Chosen representative of an isomorphism class · The trivial irreducible class

DefinitionIsomorphism classes of simple representations#✓fully proved

For a finite group \(G\), \(\mathrm{Irr}(G)\) is the set of isomorphism classes of simple finite-dimensional complex representations of \(G\).

def Irr : Type 1 := Quotient (Simple.isoSetoid G)
Uses 1 · Used by 14
Statement usesIsomorphism of simple representations
Used byBound on the number of irreducible representations · Character of an isomorphism class · Character of a class via its chosen representative · Characters determine irreducible representations · Character value at the identity · Orthogonality of irreducible characters · Class functions orthogonal to all irreducible characters vanish · Expansion of class functions in irreducible characters · A simple group with a prime-power conjugacy class has prime order · Pairing of the identity indicator with a character · Column orthogonality at the identity · Chosen representative of an isomorphism class · Sum of squared degrees · The trivial irreducible class

DefinitionCharacter of an isomorphism class#✓fully proved

Let \(G\) be a group. For an isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\), the character of \(c\) is the function \(\chi_c \colon G \to \mathbb{C}\) given by \(\chi_c(g) = \operatorname{tr} \rho(g)\) for any representative \((V, \rho)\) of \(c\). It does not depend on the representative, since isomorphic representations have the same character.

noncomputable def Irr.charFun (c : Irr G) : G → ℂ :=
  Quotient.lift (fun S => S.1.character) (fun S T h => by
    obtain ⟨i⟩ := h
    exact FDRep.char_iso i) c
Uses 2 · Used by 12
Statement usesIsomorphism classes of simple representations · Isomorphism of simple representations
Used byBound on the number of irreducible representations · Character of a class via its chosen representative · Characters determine irreducible representations · Character value at the identity · Character of the trivial representation · Orthogonality of irreducible characters · Class functions orthogonal to all irreducible characters vanish · Expansion of class functions in irreducible characters · A simple group with a prime-power conjugacy class has prime order · Pairing of the identity indicator with a character · Column orthogonality at the identity · Sum of squared degrees

DefinitionChosen representative of an isomorphism class#✓fully proved

For a finite group \(G\) and an isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\), this is a simple finite-dimensional complex representation of \(G\) in the class \(c\), fixed by the axiom of choice.

noncomputable def Irr.repBundle (c : Irr G) : {V : FDRep ℂ G // Simple V} :=
  Quotient.out c
Uses 2 · Used by 4
Statement usesIsomorphism classes of simple representations · Isomorphism of simple representations
Used byCharacter of a class via its chosen representative · Character value at the identity · Orthogonality of irreducible characters · A simple group with a prime-power conjugacy class has prime order

TheoremCharacters determine irreducible representations#✓fully proved

Let \(G\) be a finite group. Two isomorphism classes of simple finite-dimensional complex representations of \(G\) that have the same character are equal.

theorem Irr.charFun_inj [Finite G] : Function.Injective (Irr.charFun G)
Uses 3 · Used by 1
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class
Proof usesIsomorphism of simple representations
Used byA simple group with a prime-power conjugacy class has prime order

DefinitionThe trivial irreducible class#✓fully proved

Let \(G\) be a finite group. The trivial representation of \(G\) on \(\mathbb{C}\), where every element of \(G\) acts as the identity, is simple, and this is its class among the isomorphism classes of simple finite-dimensional complex representations of \(G\).

noncomputable def Irr.triv : Irr G :=
  Quotient.mk _
    ⟨FDRep.of (Representation.trivial ℂ G ℂ),
      simple_fdrep_of_irreducible G (Representation.trivial ℂ G ℂ)⟩
Uses 3 · Used by 2
Statement usesIsomorphism classes of simple representations · Isomorphism of simple representations · Irreducible representations are simple
Used byCharacter of the trivial representation · A simple group with a prime-power conjugacy class has prime order

TheoremCharacter of the trivial representation#✓fully proved

Let \(G\) be a finite group. The character of the isomorphism class of the trivial representation of \(G\) on \(\mathbb{C}\) takes the value \(1\) at every \(g \in G\).

theorem Irr.charFun_triv (g : G) : Irr.charFun G (Irr.triv G) g = 1
Uses 2 · Used by 1
Statement usesCharacter of an isomorphism class · The trivial irreducible class
Used byA simple group with a prime-power conjugacy class has prime order

TheoremCharacter value at the identity#✓fully proved

Let \(G\) be a group and let \(c\) be an isomorphism class of simple finite-dimensional complex representations of \(G\). The character of \(c\) at the identity \(1 \in G\) equals the dimension over \(\mathbb{C}\) of the chosen representative of \(c\).

theorem Irr.charFun_one (c : Irr G) :
    Irr.charFun G c 1 = ((Module.finrank ℂ ↥(Irr.repBundle G c).1 : ℕ) : ℂ)
Uses 4 · Used by 1
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Chosen representative of an isomorphism class
Proof usesIsomorphism of simple representations
Used byA simple group with a prime-power conjugacy class has prime order

TheoremCharacter of a class via its chosen representative#✓fully proved

Let \(G\) be a group and let \(c\) be an isomorphism class of simple finite-dimensional complex representations of \(G\), with chosen representative \((V, \rho)\). For every \(x \in G\), the character of \(c\) at \(x\) equals the character of the representation \(\rho\) at \(x\), namely \(\operatorname{tr} \rho(x)\).

theorem Irr.charFun_eq_repBundle_char (c : Irr G) (x : G) :
    Irr.charFun G c x = Representation.character
      ((Irr.repBundle G c).1.ρ : Representation ℂ G ↥(Irr.repBundle G c).1) x
Uses 4 · Used by 1
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Chosen representative of an isomorphism class
Proof usesIsomorphism of simple representations
Used byA simple group with a prime-power conjugacy class has prime order

TheoremOrthogonality of irreducible characters#✓fully proved

Let \(G\) be a finite group and let \(\chi_i\) and \(\chi_j\) be the characters of isomorphism classes \(i\) and \(j\) of simple finite-dimensional complex representations of \(G\). Then

\[\frac{1}{|G|} \sum_{g \in G} \chi_i(g)\, \chi_j(g^{-1}) = \begin{cases} 1 & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases}\]
theorem charInner_orth (i j : Irr G) :
    (Nat.card G : ℂ)⁻¹ * ∑ g : G, Irr.charFun G i g * Irr.charFun G j g⁻¹ =
      if i = j then 1 else 0
Uses 4 · Used by 2
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class
Proof usesChosen representative of an isomorphism class · Isomorphism of simple representations
Used byBound on the number of irreducible representations · Expansion of class functions in irreducible characters

DefinitionClass function#✓fully proved

A function \(f \colon G \to \mathbb{C}\) on a finite group \(G\) is a class function when \(f(hgh^{-1}) = f(g)\) for all \(g, h \in G\), that is, when \(f\) is constant on conjugacy classes.

def IsClassFun (f : G → ℂ) : Prop := ∀ g h : G, f (h * g * h⁻¹) = f g
Used by 5
Used byClass functions orthogonal to all irreducible characters vanish · Expansion of class functions in irreducible characters · Column orthogonality at the identity · Sum of squared degrees · The averaging operator of a class function is \(G\)-equivariant

TheoremBound on the number of irreducible representations#✓fully proved

Let \(G\) be a finite group. Every finite set of isomorphism classes of simple finite-dimensional complex representations of \(G\) has at most \(|G|\) elements.

theorem cardBound (s : Finset (Irr G)) : s.card ≤ Fintype.card G
Uses 3 · Used by 4
Statement usesIsomorphism classes of simple representations
Proof usesCharacter of an isomorphism class · Orthogonality of irreducible characters
Used byExpansion of class functions in irreducible characters · A simple group with a prime-power conjugacy class has prime order · Column orthogonality at the identity · Sum of squared degrees

DefinitionZimmerman's averaging operator#✓fully proved

Let \(G\) be a finite group, let \(M\) be a module over the group algebra \(\mathbb{C}[G]\) with a compatible \(\mathbb{C}\)-module structure, and write \(\rho(g)\) for the action of \(g \in G\) on \(M\). For a function \(f : G \to \mathbb{C}\), the averaging operator of \(f\) is the \(\mathbb{C}\)-linear endomorphism \(T_f = \sum_{g \in G} f(g)\,\rho(g^{-1})\) of \(M\).

noncomputable def zimmOp (M : Type*) [AddCommGroup M] [Module (MonoidAlgebra ℂ G) M]
    [Module ℂ M] [IsScalarTower ℂ (MonoidAlgebra ℂ G) M] (f : G → ℂ) :
    Module.End ℂ M :=
  ∑ g : G, f g • (Representation.ofModule' (k := ℂ) M) g⁻¹
Used by 2
Used byClass functions orthogonal to all irreducible characters vanish · The averaging operator of a class function is \(G\)-equivariant

TheoremThe averaging operator of a class function is \(G\)-equivariant#✓fully proved

Let \(G\) be a finite group, let \(M\) be a module over the group algebra \(\mathbb{C}[G]\) with a compatible \(\mathbb{C}\)-module structure, and write \(\rho(h)\) for the action of \(h \in G\) on \(M\). If \(f : G \to \mathbb{C}\) is a class function, then its averaging operator \(T_f = \sum_{g \in G} f(g)\,\rho(g^{-1})\) satisfies \(\rho(h)(T_f x) = T_f(\rho(h) x)\) for all \(h \in G\) and \(x \in M\).

theorem zimmOp_comm (M : Type*) [AddCommGroup M] [Module (MonoidAlgebra ℂ G) M]
    [Module ℂ M] [IsScalarTower ℂ (MonoidAlgebra ℂ G) M]
    (f : G → ℂ) (hf : IsClassFun G f) (h : G) (x : M) :
    (Representation.ofModule' (k := ℂ) M) h (zimmOp G M f x) =
      zimmOp G M f ((Representation.ofModule' (k := ℂ) M) h x)
Uses 2 · Used by 1
Statement usesClass function · Zimmerman's averaging operator
Used byClass functions orthogonal to all irreducible characters vanish

TheoremClass functions orthogonal to all irreducible characters vanish#✓fully proved

Let \(G\) be a finite group and let \(f \colon G \to \mathbb{C}\) be a class function, that is, \(f(hgh^{-1}) = f(g)\) for all \(g, h \in G\). Suppose that for every isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\), with character \(\chi_c\),

\[\frac{1}{|G|} \sum_{g \in G} f(g)\, \chi_c(g^{-1}) = 0.\]

Then \(f = 0\).

theorem classfun_eq_zero_of_orth {f : G → ℂ} (hf : IsClassFun G f)
    (horth : ∀ c : Irr G,
      (Nat.card G : ℂ)⁻¹ * ∑ g : G, f g * Irr.charFun G c g⁻¹ = 0) :
    f = 0
Sources
  • Zimmerman, Theorem 5 (core step).
Uses 7 · Used by 1
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Class function
Proof usesIsomorphism of simple representations · Irreducible representations are simple · Zimmerman's averaging operator · The averaging operator of a class function is \(G\)-equivariant
Used byExpansion of class functions in irreducible characters

TheoremExpansion of class functions in irreducible characters#✓fully proved

Let \(G\) be a finite group, let \(f \colon G \to \mathbb{C}\) be a class function, and for each of the finitely many isomorphism classes \(c\) of simple finite-dimensional complex representations of \(G\) let \(\chi_c\) be its character. Then

\[f = \sum_{c} \Big(\frac{1}{|G|} \sum_{g \in G} f(g)\, \chi_c(g^{-1})\Big)\, \chi_c,\]

where \(c\) runs over all these isomorphism classes.

theorem classfun_expand {f : G → ℂ} (hf : IsClassFun G f) :
    f = ∑ c : Irr G, ((Nat.card G : ℂ)⁻¹ * ∑ g : G, f g * Irr.charFun G c g⁻¹) •
      Irr.charFun G c
Sources
  • Zimmerman, Proposition 4 (setup).
Uses 7 · Used by 2
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Class function · Bound on the number of irreducible representations
Proof usesIsomorphism of simple representations · Orthogonality of irreducible characters · Class functions orthogonal to all irreducible characters vanish
Used byColumn orthogonality at the identity · Sum of squared degrees

DefinitionDelta function at the identity#✓fully proved

For a finite group \(G\), \(\delta_1 \colon G \to \mathbb{C}\) is the function with \(\delta_1(1) = 1\) and \(\delta_1(g) = 0\) for every \(g \ne 1\).

noncomputable def deltaOne : G → ℂ := fun g => if g = 1 then 1 else 0
Used by 3
Used byPairing of the identity indicator with a character · Column orthogonality at the identity · Sum of squared degrees

TheoremPairing of the identity indicator with a character#✓fully proved

Let \(G\) be a finite group, let \(\delta \colon G \to \mathbb{C}\) be the indicator function of the identity, so \(\delta(1) = 1\) and \(\delta(g) = 0\) for \(g \neq 1\), and let \(\chi_c\) be the character of an isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\). Then

\[\frac{1}{|G|} \sum_{g \in G} \delta(g)\, \chi_c(g^{-1}) = \frac{\chi_c(1)}{|G|}.\]
theorem deltaOne_inner (c : Irr G) :
    (Nat.card G : ℂ)⁻¹ * ∑ g : G, deltaOne G g * Irr.charFun G c g⁻¹ =
      (Nat.card G : ℂ)⁻¹ * Irr.charFun G c 1
Uses 3 · Used by 2
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Delta function at the identity
Used byColumn orthogonality at the identity · Sum of squared degrees

TheoremColumn orthogonality at the identity#✓fully proved

Let \(G\) be a finite group and, for each isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\), let \(\chi_c\) be its character. For every \(g \in G\) with \(g \ne 1\), \(\sum_c \chi_c(1)\,\chi_c(g) = 0\), where the sum runs over all such classes \(c\).

Equivalently, the character of the regular representation vanishes away from the identity.

theorem regular_character_vanishes (g : G) (hg : g ≠ 1) :
    ∑ c : Irr G, Irr.charFun G c 1 * Irr.charFun G c g = 0
Uses 7 · Used by 1
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Bound on the number of irreducible representations
Proof usesClass function · Expansion of class functions in irreducible characters · Delta function at the identity · Pairing of the identity indicator with a character
Used byA simple group with a prime-power conjugacy class has prime order

TheoremSum of squared degrees#✓fully proved

Let \(G\) be a finite group and, for each isomorphism class \(c\) of simple finite-dimensional complex representations of \(G\), let \(\chi_c\) be its character. Then \(\sum_c \chi_c(1)^2 = |G|\), where the sum runs over all such classes \(c\).

theorem sum_deg_sq : ∑ c : Irr G, (Irr.charFun G c 1) ^ 2 = (Fintype.card G : ℂ)
Uses 7
Statement usesIsomorphism classes of simple representations · Character of an isomorphism class · Bound on the number of irreducible representations
Proof usesClass function · Expansion of class functions in irreducible characters · Delta function at the identity · Pairing of the identity indicator with a character

DefinitionCyclotomic subfield of \(\mathbb{C}\)#✓fully proved

For a natural number \(m\), the \(m\)-th cyclotomic field is the intermediate field of \(\mathbb{C}/\mathbb{Q}\) generated over \(\mathbb{Q}\) by the \(m\)-th roots of unity, that is, by the complex roots of \(X^m - 1\).

For \(m = 0\) the polynomial \(X^0 - 1\) is zero and is taken to have no roots, so the field is \(\mathbb{Q}\).

noncomputable def cycSubfield (m : ℕ) : IntermediateField ℚ ℂ :=
  IntermediateField.adjoin ℚ ↑(Polynomial.nthRootsFinset m (1 : ℂ))
Used by 6
Used byCharacter vanishing from coprimality and a strict norm bound · Character values lie in a cyclotomic field · Characteristic roots as elements of the cyclotomic field · The \(m\)-th cyclotomic field is a splitting field of \(X^m - 1\) · The zeroth cyclotomic field is \(\mathbb{Q}\) · Field embeddings applied to character values

Theorem\(X^m - 1\) over \(\mathbb{Q}\) and over \(\mathbb{C}\)#✓fully proved

For every natural number \(m\), mapping the coefficients of the rational polynomial \(X^m - 1\) along the inclusion \(\mathbb{Q} \to \mathbb{C}\) gives the complex polynomial \(X^m - 1\).

theorem map_X_pow_sub_C_rat (m : ℕ) :
    ((X ^ m - C 1 : ℚ[X]).map (algebraMap ℚ ℂ)) = (X ^ m - C 1 : ℂ[X])
Used by 2
Used byThe \(m\)-th cyclotomic field is a splitting field of \(X^m - 1\) · Complex roots of \(X^m - 1\)

TheoremComplex roots of \(X^m - 1\)#✓fully proved

For every natural number \(m \neq 0\), the set of complex roots of the rational polynomial \(X^m - 1\) is exactly the set of \(m\)-th roots of unity in \(\mathbb{C}\).

theorem cyc_rootSet (m : ℕ) (hm : m ≠ 0) :
    (X ^ m - C 1 : ℚ[X]).rootSet ℂ =
      ↑(Polynomial.nthRootsFinset m (1 : ℂ))
Uses 1 · Used by 1
Proof uses\(X^m - 1\) over \(\mathbb{Q}\) and over \(\mathbb{C}\)
Used byThe \(m\)-th cyclotomic field is a splitting field of \(X^m - 1\)

TheoremThe \(m\)-th cyclotomic field is a splitting field of \(X^m - 1\)#✓fully proved

For every natural number \(m \neq 0\), the subfield of \(\mathbb{C}\) generated over \(\mathbb{Q}\) by the \(m\)-th roots of unity is a splitting field over \(\mathbb{Q}\) of the polynomial \(X^m - 1 \in \mathbb{Q}[X]\).

theorem cyc_isSplitting (m : ℕ) (hm : m ≠ 0) :
    (X ^ m - C 1 : ℚ[X]).IsSplittingField ℚ (cycSubfield m)
Uses 3 · Used by 1
Statement usesCyclotomic subfield of \(\mathbb{C}\)
Proof usesComplex roots of \(X^m - 1\) · \(X^m - 1\) over \(\mathbb{Q}\) and over \(\mathbb{C}\)
Used byCharacter vanishing from coprimality and a strict norm bound

TheoremThe zeroth cyclotomic field is \(\mathbb{Q}\)#✓fully proved

For \(m = 0\) the cyclotomic subfield of \(\mathbb{C}\) is the bottom intermediate field, that is \(\mathbb{Q}\) itself: the polynomial \(X^0 - 1\) is zero and is taken to have no roots, so nothing is adjoined.

theorem cycSubfield_zero : cycSubfield 0 = ⊥
Uses 1 · Used by 1
Statement usesCyclotomic subfield of \(\mathbb{C}\)
Used byCharacter vanishing from coprimality and a strict norm bound

DefinitionConjugacy class#✓fully proved

For an element \(g\) of a finite group \(G\), the conjugacy class of \(g\) is the finite set \(\{h g h^{-1} : h \in G\}\), the orbit of \(g\) under the action of \(G\) on itself by conjugation.

noncomputable def conjClass (g : G) : Finset G :=
  (MulAction.orbit (ConjAct G) g).toFinset
Used by 21
Used byBurnside's vanishing theorem for coprime class sizes · Burnside's \(p^a q^b\) theorem from the prime-power class corollary · Burnside's \(p^a q^b\) theorem in the lowest universe · Conjugacy class of the chosen representative · Central scalars multiply via the class structure constants · Integrality of the normalized character value at a coprime class · Character vanishing from coprimality and a strict norm bound · Nonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size · Class sums of conjugacy classes are central · Class sums commute with group elements · The class sum of the conjugacy class of an element is central · Class size times character ratio is an algebraic integer · Products of class sums expand in class sums · Class size times centralizer order · Orbit–stabilizer for a conjugacy class · Conjugate elements have the same conjugacy class · Conjugacy classes are closed under conjugation · A simple group with a prime-power conjugacy class has prime order · A nontrivial element whose class size is a power of \(p\) · Products of central-scalar generators stay in their span · Class structure constants are class functions

TheoremOrbit–stabilizer for a conjugacy class#✓fully proved

For every element \(g\) of a finite group \(G\), the size of the conjugacy class of \(g\) times the order of the stabilizer of \(g\) under the action of \(G\) on itself by conjugation, \(x \cdot y = x y x^{-1}\), equals the order of \(G\).

theorem conjClass_card_mul_stabilizer_card (g : G) :
    (conjClass g).card * Fintype.card (MulAction.stabilizer (ConjAct G) g) =
      Fintype.card G
Uses 1 · Used by 1
Statement usesConjugacy class
Used byClass size times centralizer order

DefinitionCentralizer as a conjugation stabilizer#✓fully proved

For an element \(g\) of a finite group \(G\), this is the bijection from the centralizer \(C_G(g) = \{x \in G : xg = gx\}\) onto the stabilizer of \(g\) for the action of \(G\) on itself by conjugation, \(x \cdot y = x y x^{-1}\), that sends each element \(x\) to itself.

def centralizerEquivStabilizer (g : G) :
    Subgroup.centralizer {g} ≃ MulAction.stabilizer (ConjAct G) g :=
  Equiv.subtypeEquiv ConjAct.toConjAct.toEquiv (fun x => by
    rw [Subgroup.mem_centralizer_iff]
    simp only [Set.mem_singleton_iff, forall_eq]
    rw [MulAction.mem_stabilizer_iff]
    change g * x = x * g ↔ ConjAct.toConjAct x • g = g
    rw [ConjAct.toConjAct_smul, mul_inv_eq_iff_eq_mul]
    exact eq_comm)
Used by 1
Used byClass size times centralizer order

TheoremClass size times centralizer order#✓fully proved

Let \(g\) be an element of a finite group \(G\), let \(g^G\) be its conjugacy class and let \(C_G(g) = \{x \in G : xg = gx\}\) be its centralizer. Then \(|g^G| \cdot |C_G(g)| = |G|\).

theorem conjClass_card_mul_centralizer_card (g : G) :
    (conjClass g).card * Fintype.card (Subgroup.centralizer {g}) = Fintype.card G
Uses 3 · Used by 1
Statement usesConjugacy class
Proof usesCentralizer as a conjugation stabilizer · Orbit–stabilizer for a conjugacy class
Used byA nontrivial element whose class size is a power of \(p\)

TheoremConjugacy classes are closed under conjugation#✓fully proved

Let \(g\), \(h\) and \(x\) be elements of a finite group \(G\). If \(x\) lies in the conjugacy class of \(g\), then so does \(h x h^{-1}\).

theorem conj_mem_conjClass (g h x : G) (hx : x ∈ conjClass g) :
    h * x * h⁻¹ ∈ conjClass g
Uses 1 · Used by 3
Statement usesConjugacy class
Used byBurnside's \(p^a q^b\) theorem from the prime-power class corollary · Class sums commute with group elements · Class structure constants are class functions

TheoremA nontrivial element whose class size is a power of \(p\)#✓fully proved

Let \(p\) and \(q\) be primes, let \(a\) and \(b\) be natural numbers with \(b \ge 1\), and let \(G\) be a finite group of order \(p^a q^b\). Then there are an element \(g \ne 1\) of \(G\) and a natural number \(k \le a\) such that the conjugacy class of \(g\) has exactly \(p^k\) elements.

In the proof, \(g\) is a nontrivial element of the center of a subgroup of \(G\) of order \(q^b\) (a Sylow \(q\)-subgroup when \(p \ne q\)).

theorem exists_ne_one_class_prime_pow {p q a b : ℕ} (hp : p.Prime)
    (hq : q.Prime) (hcard : Fintype.card G = p ^ a * q ^ b) (hb : 1 ≤ b) :
    ∃ g : G, g ≠ 1 ∧ ∃ k ≤ a, (conjClass g).card = p ^ k
Uses 2 · Used by 1
Statement usesConjugacy class
Proof usesClass size times centralizer order
Used byBurnside's \(p^a q^b\) theorem from the prime-power class corollary

DefinitionClass sum of a finite subset#✓fully proved

Let \(G\) be a group. The class sum of a finite subset \(C \subseteq G\) is the element \(\widehat{C} = \sum_{x \in C} x\) of the complex group algebra \(\mathbb{C}[G]\).

noncomputable def classSum (C : Finset G) : MonoidAlgebra ℂ G :=
  ∑ x ∈ C, MonoidAlgebra.of ℂ G x
Used by 8
Used byCentral scalar of a conjugacy class · Central scalars multiply via the class structure constants · Trace formula for central scalars · Class sums of conjugacy classes are central · Class sums commute with group elements · The class sum of the conjugacy class of an element is central · Products of class sums expand in class sums · Coefficients of a product of class sums

TheoremClass sums commute with group elements#✓fully proved

Let \(G\) be a finite group, let \(g \in G\), and let \(\widehat{C_g} = \sum_{x \in C_g} x\) be the sum, in the complex group algebra \(\mathbb{C}[G]\), of the elements of the conjugacy class \(C_g\) of \(g\). Then \(\widehat{C_g} h = h \widehat{C_g}\) for every \(h \in G\), where \(h\) is viewed as a basis element of \(\mathbb{C}[G]\).

theorem classSum_central (g h : G) :
    classSum (conjClass g) * MonoidAlgebra.of ℂ G h =
      MonoidAlgebra.of ℂ G h * classSum (conjClass g)
Uses 3 · Used by 1
Statement usesClass sum of a finite subset · Conjugacy class
Proof usesConjugacy classes are closed under conjugation
Used byThe class sum of the conjugacy class of an element is central

TheoremThe class sum of the conjugacy class of an element is central#✓fully proved

Let \(G\) be a finite group, let \(g \in G\), and let \(\widehat{C_g} = \sum_{x \in C_g} x\) be the sum, in the complex group algebra \(\mathbb{C}[G]\), of the elements of the conjugacy class \(C_g\) of \(g\). Then \(w \widehat{C_g} = \widehat{C_g} w\) for every \(w \in \mathbb{C}[G]\).

theorem classSum_central' (g : G) (w : MonoidAlgebra ℂ G) :
    w * classSum (conjClass g) = classSum (conjClass g) * w
Uses 3 · Used by 1
Statement usesClass sum of a finite subset · Conjugacy class
Proof usesClass sums commute with group elements
Used byClass sums of conjugacy classes are central

DefinitionChosen representative of a conjugacy class#✓fully proved

For each conjugacy class \(K\) of a group \(G\), the representative of \(K\) is an element \(g_K \in G\), fixed once and for all by choice, whose conjugacy class is \(K\).

noncomputable def classRep (l : ConjClasses G) : G :=
  Classical.choose (ConjClasses.mk_surjective l)
Used by 11
Used byConjugacy class of the chosen representative · Central scalars multiply via the class structure constants · Characters are constant on conjugacy classes · Characters at inverses are constant on conjugacy classes · Contribution of a conjugacy class to the self-pairing sum · Class sums of conjugacy classes are central · Class size times character ratio is an algebraic integer · Products of class sums expand in class sums · Members of a conjugacy class are conjugate to its representative · Degrees of irreducible representations divide the group order · Products of central-scalar generators stay in their span

TheoremConjugacy class of the chosen representative#✓fully proved

Let \(G\) be a finite group. For every conjugacy class \(K\) of \(G\), the set of elements of \(K\) equals the conjugacy class of the chosen representative of \(K\).

theorem carrier_toFinset (l : ConjClasses G) :
    (ConjClasses.carrier l).toFinset = conjClass (classRep l)
Uses 2 · Used by 3
Statement usesChosen representative of a conjugacy class · Conjugacy class
Used byCentral scalars multiply via the class structure constants · Class sums of conjugacy classes are central · Class size times character ratio is an algebraic integer

DefinitionStructure constants of a pair of subsets#✓fully proved

Let \(G\) be a finite group. For finite subsets \(C_i, C_j \subseteq G\) and an element \(z \in G\), the structure constant is the number of pairs \((x, y) \in C_i \times C_j\) with \(xy = z\).

noncomputable def structConst (Ci Cj : Finset G) (z : G) : ℕ :=
  ((Ci.product Cj).filter (fun p => p.1 * p.2 = z)).card
Used by 5
Used byCentral scalars multiply via the class structure constants · Products of class sums expand in class sums · Coefficients of a product of class sums · Products of central-scalar generators stay in their span · Class structure constants are class functions

TheoremClass structure constants are class functions#✓fully proved

Let \(G\) be a finite group, let \(g_i, g_j \in G\) with conjugacy classes \(C_{g_i}\) and \(C_{g_j}\), and for \(z \in G\) let \(a(z)\) be the number of pairs \((x, y) \in C_{g_i} \times C_{g_j}\) with \(x y = z\). If \(u, z \in G\) are conjugate, then \(a(u) = a(z)\).

theorem structConst_conj (gi gj u z : G) (h : IsConj u z) :
    structConst (conjClass gi) (conjClass gj) u =
      structConst (conjClass gi) (conjClass gj) z
Uses 3 · Used by 1
Statement usesConjugacy class · Structure constants of a pair of subsets
Proof usesConjugacy classes are closed under conjugation
Used byProducts of class sums expand in class sums

TheoremCoefficients of a product of class sums#✓fully proved

Let \(G\) be a group, let \(C_i\) and \(C_j\) be finite subsets of \(G\), and write \(\widehat{C} = \sum_{x \in C} x\) in the complex group algebra \(\mathbb{C}[G]\). For every \(u \in G\), the coefficient of \(u\) in \(\widehat{C_i} \widehat{C_j}\) is the number of pairs \((x, y) \in C_i \times C_j\) with \(x y = u\).

theorem coeff_classSum_mul (Ci Cj : Finset G) (u : G) :
    (classSum Ci * classSum Cj).coeff u = (structConst Ci Cj u : ℂ)
Uses 2 · Used by 1
Statement usesClass sum of a finite subset · Structure constants of a pair of subsets
Used byProducts of class sums expand in class sums

TheoremProducts of class sums expand in class sums#✓fully proved

Let \(G\) be a finite group. For a finite subset \(C\) of \(G\) write \(\widehat{C} = \sum_{x \in C} x\) in the complex group algebra \(\mathbb{C}[G]\), and for \(g \in G\) let \(C_g\) be its conjugacy class. Let \(g_i, g_j \in G\), and for each conjugacy class \(K\) of \(G\) with chosen representative \(z_K\) let \(a_K\) be the number of pairs \((x, y) \in C_{g_i} \times C_{g_j}\) with \(x y = z_K\). Then \(\widehat{C_{g_i}} \widehat{C_{g_j}} = \sum_K a_K \widehat{K}\), the sum running over all conjugacy classes \(K\) of \(G\).

theorem classSum_mul (gi gj : G) :
    classSum (conjClass gi) * classSum (conjClass gj)
      = ∑ l : ConjClasses G, (structConst (conjClass gi) (conjClass gj) (classRep l) : ℂ)
          • classSum (ConjClasses.carrier l).toFinset
Uses 6 · Used by 1
Statement usesChosen representative of a conjugacy class · Class sum of a finite subset · Conjugacy class · Structure constants of a pair of subsets
Proof usesCoefficients of a product of class sums · Class structure constants are class functions
Used byCentral scalars multiply via the class structure constants

TheoremConjugate elements have the same conjugacy class#✓fully proved

Let \(G\) be a finite group. If \(g_1, g_2 \in G\) are conjugate, then the conjugacy class of \(g_1\) equals the conjugacy class of \(g_2\).

theorem conjClass_eq_of_isConj {g1 g2 : G} (h : IsConj g1 g2) :
    conjClass g1 = conjClass g2
Uses 1 · Used by 1
Statement usesConjugacy class
Used byClass size times character ratio is an algebraic integer

TheoremClass sums of conjugacy classes are central#✓fully proved

Let \(G\) be a finite group. For every conjugacy class \(K\) of \(G\) and every element \(w\) of the complex group algebra \(\mathbb{C}[G]\), the class sum \(\widehat{K} = \sum_{x \in K} x\) satisfies \(w \widehat{K} = \widehat{K} w\).

theorem classSum_carrier_central (l : ConjClasses G) (w : MonoidAlgebra ℂ G) :
    w * classSum (ConjClasses.carrier l).toFinset
      = classSum (ConjClasses.carrier l).toFinset * w
Uses 5 · Used by 3
Statement usesClass sum of a finite subset
Proof usesConjugacy class of the chosen representative · Chosen representative of a conjugacy class · The class sum of the conjugacy class of an element is central · Conjugacy class
Used byCentral scalar of a conjugacy class · Central scalars multiply via the class structure constants · Trace formula for central scalars

TheoremSchur's lemma for central elements of the group algebra#✓fully proved

Let \(\rho\) be an irreducible representation of a group \(G\) on a finite-dimensional complex vector space \(V\), extended linearly to the group algebra \(\mathbb{C}[G]\). If \(z \in \mathbb{C}[G]\) commutes with every element of \(\mathbb{C}[G]\), then \(z\) acts on \(V\) as a scalar: there is \(c \in \mathbb{C}\) with \(\rho(z) v = c\, v\) for all \(v \in V\).

theorem exists_scalar_of_central {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ]
    (z : MonoidAlgebra ℂ G) (hz : ∀ w, w * z = z * w) :
    ∃ c : ℂ, ∀ v : V, ρ.asAlgebraHom z v = c • v
Used by 3
Used byCentral scalar of a conjugacy class · Central scalars multiply via the class structure constants · Trace formula for central scalars

DefinitionCentral scalar of a conjugacy class#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\). For a conjugacy class \(C\) of \(G\), the class sum \(\sum_{x \in C} x\) is central in the group algebra \(\mathbb{C}[G]\), so it acts on \(V\) as multiplication by a complex number. The central scalar \(\omega_\rho(C)\) is that number: \(\rho\bigl(\sum_{x \in C} x\bigr) v = \omega_\rho(C)\, v\) for all \(v \in V\).

noncomputable def centralScalar (l : ConjClasses G) : ℂ :=
  Classical.choose
    (exists_scalar_of_central ρ (classSum (ConjClasses.carrier l).toFinset)
      (classSum_carrier_central l))
Uses 3 · Used by 9
Statement usesClass sum of a finite subset · Class sums of conjugacy classes are central · Schur's lemma for central elements of the group algebra
Used byCentral scalars are algebraic integers · Central scalars multiply via the class structure constants · Trace formula for central scalars · Contribution of a conjugacy class to the self-pairing sum · Class size times character ratio is an algebraic integer · Degrees of irreducible representations divide the group order · Generators of the central-scalar ring · Products of central-scalar generators stay in their span · Ring generated by the central scalars

TheoremCentral scalars multiply via the class structure constants#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(\omega_\rho(C)\) be the scalar by which the class sum of a conjugacy class \(C\) acts on \(V\). Fix a representative \(g_C\) of each conjugacy class \(C\). For conjugacy classes \(C_1\) and \(C_2\),

\[\omega_\rho(C_1)\,\omega_\rho(C_2) = \sum_{C} a_{C_1 C_2}^{C}\, \omega_\rho(C),\]

where \(C\) runs over all conjugacy classes of \(G\) and \(a_{C_1 C_2}^{C}\) is the number of pairs \((x, y) \in C_1 \times C_2\) with \(x y = g_C\).

theorem centralScalar_mul (l1 l2 : ConjClasses G) :
    centralScalar ρ l1 * centralScalar ρ l2
      = ∑ l, (structConst (conjClass (classRep l1)) (conjClass (classRep l2))
          (classRep l) : ℂ) * centralScalar ρ l
Uses 9 · Used by 1
Statement usesCentral scalar of a conjugacy class · Chosen representative of a conjugacy class · Conjugacy class · Structure constants of a pair of subsets
Proof usesConjugacy class of the chosen representative · Class sum of a finite subset · Class sums of conjugacy classes are central · Products of class sums expand in class sums · Schur's lemma for central elements of the group algebra
Used byProducts of central-scalar generators stay in their span

TheoremTrace formula for central scalars#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\) with character \(\chi\), and let \(\omega_\rho(C)\) be the scalar by which the class sum of a conjugacy class \(C\) acts on \(V\). Then \(\omega_\rho(C) \cdot \dim V = \sum_{x \in C} \chi(x)\).

theorem centralScalar_trace (l : ConjClasses G) :
    centralScalar ρ l * Module.finrank ℂ V
      = ∑ x ∈ (ConjClasses.carrier l).toFinset, ρ.character x
Uses 4 · Used by 2
Statement usesCentral scalar of a conjugacy class
Proof usesClass sum of a finite subset · Class sums of conjugacy classes are central · Schur's lemma for central elements of the group algebra
Used byContribution of a conjugacy class to the self-pairing sum · Class size times character ratio is an algebraic integer

DefinitionGenerators of the central-scalar ring#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(\omega_\rho(C)\) be the scalar by which the class sum of a conjugacy class \(C\) acts on \(V\). The set \(S_\rho\) is the finite set of complex numbers consisting of \(1\) and the values \(\omega_\rho(C)\) for all conjugacy classes \(C\) of \(G\).

noncomputable def scalarGens : Finset ℂ :=
  insert 1 (Finset.univ.image (centralScalar ρ))
Uses 1 · Used by 3
Statement usesCentral scalar of a conjugacy class
Used byCentral scalars are algebraic integers · Products of central-scalar generators stay in their span · Ring generated by the central scalars

TheoremProducts of central-scalar generators stay in their span#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(S_\rho\) be the finite set of complex numbers consisting of \(1\) and the scalars by which the class sums of the conjugacy classes of \(G\) act on \(V\). If \(a, b \in S_\rho\), then \(ab\) lies in the \(\mathbb{Z}\)-linear span of \(S_\rho\).

theorem scalarGens_mul (a b : ℂ) (ha : a ∈ scalarGens ρ) (hb : b ∈ scalarGens ρ) :
    a * b ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ)
Uses 6 · Used by 1
Statement usesGenerators of the central-scalar ring
Proof usesCentral scalar of a conjugacy class · Central scalars multiply via the class structure constants · Chosen representative of a conjugacy class · Conjugacy class · Structure constants of a pair of subsets
Used byRing generated by the central scalars

DefinitionRing generated by the central scalars#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(S_\rho\) be the finite set of complex numbers consisting of \(1\) and the scalars by which the class sums of the conjugacy classes of \(G\) act on \(V\). The \(\mathbb{Z}\)-linear span of \(S_\rho\) is closed under multiplication, and this is that span as a \(\mathbb{Z}\)-subalgebra of \(\mathbb{C}\).

BurnsidePaqb.scalarSubalg · 43 lines 
noncomputable def scalarSubalg : Subalgebra ℤ ℂ where
  carrier := ↑(Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ))
  mul_mem' := by
    intro x y hx hy
    have hx' : x ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) := hx
    have hy' : y ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) := hy
    suffices h : x * y ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) from h
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hx'
    · intro z hz
      refine Submodule.span_induction ?_ ?_ ?_ ?_ hy'
      · intro w hw
        exact scalarGens_mul ρ z w (Finset.mem_coe.mp hz) (Finset.mem_coe.mp hw)
      · rw [mul_zero]
        exact Submodule.zero_mem _
      · intro a b ha hb iha ihb
        rw [mul_add]
        exact add_mem iha ihb
      · intro c b hb ih
        rw [mul_smul_comm]
        exact Submodule.smul_mem _ _ ih
    · rw [zero_mul]
      exact Submodule.zero_mem _
    · intro a b ha hb iha ihb
      rw [add_mul]
      exact add_mem iha ihb
    · intro c a ha ih
      rw [smul_mul_assoc]
      exact Submodule.smul_mem _ _ ih
  one_mem' := one_mem_scalarSpan ρ
  add_mem' := by
    intro x y hx hy
    have hx' : x ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) := hx
    have hy' : y ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) := hy
    have h : x + y ∈ Submodule.span ℤ (↑(scalarGens ρ) : Set ℂ) :=
      Submodule.add_mem _ hx' hy'
    exact h
  zero_mem' := Submodule.zero_mem _
  algebraMap_mem' := by
    intro n
    have h1 : algebraMap ℤ ℂ n = n • (1 : ℂ) := by
      rw [Algebra.smul_def, mul_one]
    rw [h1]
    exact Submodule.smul_mem _ _ (one_mem_scalarSpan ρ)
Uses 3 · Used by 1
Statement usesCentral scalar of a conjugacy class · Generators of the central-scalar ring · Products of central-scalar generators stay in their span
Used byCentral scalars are algebraic integers

TheoremCentral scalars are algebraic integers#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\). For every conjugacy class \(C\) of \(G\), the complex number \(\omega_\rho(C)\) by which the class sum \(\sum_{x \in C} x\) acts on \(V\) is an algebraic integer, that is, integral over \(\mathbb{Z}\).

theorem centralScalar_isIntegral (l : ConjClasses G) :
    IsIntegral ℤ (centralScalar ρ l)
Uses 3 · Used by 2
Statement usesCentral scalar of a conjugacy class
Proof usesGenerators of the central-scalar ring · Ring generated by the central scalars
Used byClass size times character ratio is an algebraic integer · Degrees of irreducible representations divide the group order

TheoremClass size times character ratio is an algebraic integer#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), with character \(\chi\). For every \(g \in G\), if \(C\) is the conjugacy class of \(g\), then \(|C|\,\chi(g)/\chi(1)\) is an algebraic integer.

theorem classSum_centralScalar_isIntegral (g : G) :
    IsIntegral ℤ ((conjClass g).card * ρ.character g / ρ.character 1)
Sources
  • Bielefeld Prop 1.
Uses 7 · Used by 1
Statement usesConjugacy class
Proof usesConjugacy class of the chosen representative · Central scalar of a conjugacy class · Central scalars are algebraic integers · Trace formula for central scalars · Chosen representative of a conjugacy class · Conjugate elements have the same conjugacy class
Used byIntegrality of the normalized character value at a coprime class

TheoremCharacter value as the sum of characteristic roots#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a finite-dimensional complex vector space, with character \(\chi\), and let \(g \in G\). Then \(\chi(g)\) is the sum of the roots of the characteristic polynomial of \(\rho(g)\), counted with multiplicity.

theorem character_eq_sum_roots {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) :
    ρ.character g = (ρ g).charpoly.roots.sum
Used by 6
Used byCharacters of full absolute value have equal eigenvalues · Burnside's vanishing theorem for coprime class sizes · Character values lie in a cyclotomic field · Characteristic roots are not all equal below the degree · Character values are algebraic integers · Field embeddings applied to character values

TheoremCharacteristic roots are killed by the order of the element#✓fully proved

Let \(G\) be a group, \(V\) a finite-dimensional complex vector space, \(\rho\) a representation of \(G\) on \(V\), and \(g \in G\) an element of order \(n\), where \(n = 0\) if \(g\) has infinite order. Then every root \(\mu\) of the characteristic polynomial of \(\rho(g)\) satisfies \(\mu^n = 1\); in particular, when \(g\) has finite order, \(\mu\) is a root of unity.

theorem charpoly_root_pow_orderOf {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) (μ : ℂ)
    (hμ : μ ∈ (ρ g).charpoly.roots) : μ ^ orderOf g = 1
Used by 4
Used byCharacter vanishing from coprimality and a strict norm bound · Character values lie in a cyclotomic field · Character values are algebraic integers · Eigenvalues of a finite group representation have modulus one

TheoremEigenvalues of a finite group representation have modulus one#✓fully proved

Let \(G\) be a finite group, \(V\) a finite-dimensional complex vector space and \(\rho\) a representation of \(G\) on \(V\). For every \(g \in G\), every root \(\mu\) of the characteristic polynomial of \(\rho(g)\) satisfies \(|\mu| = 1\).

theorem charpoly_root_norm_eq_one {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Finite G] (ρ : Representation ℂ G V) (g : G) (μ : ℂ)
    (hμ : μ ∈ (ρ g).charpoly.roots) : ‖μ‖ = 1
Uses 1 · Used by 3
Proof usesCharacteristic roots are killed by the order of the element
Used byCharacters of full absolute value have equal eigenvalues · Burnside's vanishing theorem for coprime class sizes · Characteristic roots are not all equal below the degree

TheoremReal part of a product with a conjugate#✓fully proved

For complex numbers \(a\) and \(b\), \(\operatorname{Re} a \operatorname{Re} b + \operatorname{Im} a \operatorname{Im} b = \operatorname{Re}(a \bar{b})\).

theorem re_mul_conj (a b : ℂ) :
    a.re * b.re + a.im * b.im = (a * starRingEnd ℂ b).re
Used by 2
Used bySum of two distinct unit complex numbers · Strict triangle inequality for unit complex numbers

TheoremProduct of a unit complex number with a conjugate unit#✓fully proved

For complex numbers \(a\) and \(b\) with \(|a| = |b| = 1\), we have \(|a \bar{b}| = 1\).

theorem norm_mul_conj_eq_one (a b : ℂ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) :
    ‖a * starRingEnd ℂ b‖ = 1
Used by 2
Used bySum of two distinct unit complex numbers · Strict triangle inequality for unit complex numbers

TheoremCancelling a unit-modulus conjugate#✓fully proved

Let \(a, b \in \mathbb{C}\) with \(|b| = 1\). If \(a \bar{b} = 1\), then \(a = b\).

theorem eq_of_mul_conj_eq_one (a b : ℂ) (hb : ‖b‖ = 1)
    (h : a * starRingEnd ℂ b = 1) : a = b
Used by 2
Used bySum of two distinct unit complex numbers · Strict triangle inequality for unit complex numbers

TheoremReal part of a unit complex number other than \(1\)#✓fully proved

If \(w \in \mathbb{C}\) satisfies \(|w| = 1\) and \(w \neq 1\), then \(\operatorname{Re} w < 1\).

theorem re_lt_one_of_ne_one (w : ℂ) (hw : ‖w‖ = 1) (hne : w ≠ 1) :
    w.re < 1
Used by 2
Used bySum of two distinct unit complex numbers · Strict triangle inequality for unit complex numbers

TheoremStrict triangle inequality for unit complex numbers#✓fully proved

Let \(\mu_1, \dots, \mu_n\) be complex numbers with \(|\mu_i| = 1\) for every \(i\), not all equal. Then \(\left|\sum_{i=1}^{n} \mu_i\right| < n\).

theorem abs_sum_roots_of_unity_lt {n : ℕ} (μ : Fin n → ℂ)
    (hmod : ∀ i, ‖μ i‖ = 1) (hne : ∃ i j, μ i ≠ μ j) :
    ‖∑ i, μ i‖ < n
Uses 4
Proof usesCancelling a unit-modulus conjugate · Product of a unit complex number with a conjugate unit · Real part of a unit complex number other than \(1\) · Real part of a product with a conjugate

TheoremCharacter values are algebraic integers#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space, with character \(\chi\). Then \(\chi(g)\) is an algebraic integer for every \(g \in G\).

Each value \(\chi(g)\) is a sum of roots of unity.

theorem character_isIntegral {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Finite G] (ρ : Representation ℂ G V) (g : G) :
    IsIntegral ℤ (ρ.character g)
Uses 2 · Used by 3
Proof usesCharacter value as the sum of characteristic roots · Characteristic roots are killed by the order of the element
Used byIntegrality of the normalized character value at a coprime class · A simple group with a prime-power conjugacy class has prime order · Degrees of irreducible representations divide the group order

TheoremIntegrality of the normalized character value at a coprime class#✓fully proved

Let \(G\) be a finite group, let \(\rho\) be an irreducible representation of \(G\) on a nonzero finite-dimensional complex vector space \(V\), with character \(\chi\), and let \(g \in G\). If the size of the conjugacy class of \(g\) is coprime to \(\dim V\), then \(\chi(g)/\chi(1)\) is an algebraic integer.

theorem charDivDeg_isIntegral_of_coprime {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] (g : G)
    (hcop : Nat.Coprime (conjClass g).card (Module.finrank ℂ V)) :
    IsIntegral ℤ (ρ.character g / ρ.character 1)
Sources
  • Bielefeld Theorem 5, integrality step.
Uses 3 · Used by 1
Statement usesConjugacy class
Proof usesCharacter values are algebraic integers · Class size times character ratio is an algebraic integer
Used byCharacter vanishing from coprimality and a strict norm bound

TheoremSum of two distinct unit complex numbers#✓fully proved

If \(a\) and \(b\) are distinct complex numbers with \(|a| = |b| = 1\), then \(|a + b| < 2\).

theorem abs_add_two_ne_unit_lt_two {a b : ℂ} (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
    (hne : a ≠ b) : ‖a + b‖ < 2
Uses 4 · Used by 1
Proof usesCancelling a unit-modulus conjugate · Product of a unit complex number with a conjugate unit · Real part of a unit complex number other than \(1\) · Real part of a product with a conjugate
Used byStrict triangle inequality for unit complex numbers, multiset form

TheoremStrict triangle inequality for unit complex numbers, multiset form#✓fully proved

Let \(s\) be a finite multiset of complex numbers, each of absolute value \(1\), containing two distinct elements. Then the absolute value of the sum of \(s\) is strictly less than the number of elements of \(s\), counted with multiplicity.

theorem abs_multiset_sum_lt (s : Multiset ℂ) (hunit : ∀ μ ∈ s, ‖μ‖ = 1)
    (hne : ∃ a ∈ s, ∃ b ∈ s, a ≠ b) : ‖s.sum‖ < s.card
Uses 1 · Used by 1
Proof usesSum of two distinct unit complex numbers
Used byCharacters of full absolute value have equal eigenvalues

TheoremNumber of characteristic roots of a representation matrix#✓fully proved

Let \(G\) be a group, \(V\) a finite-dimensional complex vector space, \(\rho\) a representation of \(G\) on \(V\) and \(g \in G\). The characteristic polynomial of \(\rho(g)\) has exactly \(\dim_{\mathbb{C}} V\) roots in \(\mathbb{C}\), counted with multiplicity.

theorem charpoly_roots_card {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) :
    (ρ g).charpoly.roots.card = Module.finrank ℂ V
Used by 6
Used byCharacters of full absolute value have equal eigenvalues · Burnside's vanishing theorem for coprime class sizes · Character vanishing from coprimality and a strict norm bound · Characteristic roots are not all equal below the degree · Nonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size · Elements with a single eigenvalue act as scalars

TheoremCharacteristic roots are not all equal below the degree#✓fully proved

Let \(G\) be a finite group, let \(\rho\) be a representation of \(G\) on a nonzero finite-dimensional complex vector space \(V\), with character \(\chi\), and let \(g \in G\). If \(|\chi(g)| < \dim V\), then the characteristic polynomial of \(\rho(g)\) has two distinct roots.

theorem char_roots_not_all_equal {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] [Finite G] (ρ : Representation ℂ G V) (g : G)
    (hlt : ‖ρ.character g‖ < Module.finrank ℂ V) :
    ∃ a ∈ (ρ g).charpoly.roots, ∃ b ∈ (ρ g).charpoly.roots, a ≠ b
Uses 3
Proof usesCharacter value as the sum of characteristic roots · Eigenvalues of a finite group representation have modulus one · Number of characteristic roots of a representation matrix

TheoremCharacter values lie in a cyclotomic field#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a finite-dimensional complex vector space, with character \(\chi\), and let \(g \in G\) have finite order \(m\). Then \(\chi(g)\) lies in the subfield of \(\mathbb{C}\) generated over \(\mathbb{Q}\) by the \(m\)-th roots of unity.

theorem char_mem_cycSubfield {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G)
    (hm : orderOf g ≠ 0) : ρ.character g ∈ cycSubfield (orderOf g)
Uses 3 · Used by 1
Statement usesCyclotomic subfield of \(\mathbb{C}\)
Proof usesCharacter value as the sum of characteristic roots · Characteristic roots are killed by the order of the element
Used byCharacter vanishing from coprimality and a strict norm bound

DefinitionCharacteristic roots as elements of the cyclotomic field#✓fully proved

Let \(m\) be a positive integer, let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(g \in G\) be such that every root \(\mu\) of the characteristic polynomial of \(\rho(g)\) satisfies \(\mu^m = 1\). Each such root \(\mu\) is regarded as an element of the subfield \(K \subseteq \mathbb{C}\) obtained by adjoining the \(m\)-th roots of unity to \(\mathbb{Q}\).

noncomputable def conjRootElem (m : ℕ) (hm : m ≠ 0)
    {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G)
    (hmg : ∀ μ ∈ (ρ g).charpoly.roots, μ ^ m = 1)
    (x : { μ : ℂ // μ ∈ (ρ g).charpoly.roots }) : cycSubfield m :=
  ⟨x.1, mem_cycSubfield_of_pow_eq_one m hm x.1 (hmg x.1 x.2)⟩
Uses 1 · Used by 2
Statement usesCyclotomic subfield of \(\mathbb{C}\)
Used byCharacter vanishing from coprimality and a strict norm bound · Field embeddings applied to character values

TheoremField embeddings applied to character values#✓fully proved

Let \(G\) be a group, \(\rho\) a representation of \(G\) on a finite-dimensional complex vector space \(V\) with character \(\chi\), let \(m\) be a positive integer, and let \(g \in G\) be such that every root \(\mu\) of the characteristic polynomial of \(\rho(g)\) satisfies \(\mu^m = 1\). Let \(K \subseteq \mathbb{C}\) be the field obtained by adjoining the \(m\)-th roots of unity to \(\mathbb{Q}\), and suppose \(\chi(g) \in K\). Then for every \(\mathbb{Q}\)-algebra homomorphism \(\sigma : K \to \mathbb{C}\) we have \(\sigma(\chi(g)) = \sum_\mu \sigma(\mu)\), where the sum runs over the roots \(\mu\) of the characteristic polynomial of \(\rho(g)\), counted with multiplicity, each regarded as an element of \(K\).

theorem embedding_char_eq_conj_sum (m : ℕ) (hm : m ≠ 0)
    {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G)
    (hmg : ∀ μ ∈ (ρ g).charpoly.roots, μ ^ m = 1)
    (hχ : ρ.character g ∈ cycSubfield m)
    (σ : cycSubfield m →ₐ[ℚ] ℂ) :
    σ ⟨ρ.character g, hχ⟩
      = (((ρ g).charpoly.roots.attach.map
        (fun x => σ (conjRootElem m hm ρ g hmg x))).sum)
Uses 3 · Used by 1
Statement usesCharacteristic roots as elements of the cyclotomic field · Cyclotomic subfield of \(\mathbb{C}\)
Proof usesCharacter value as the sum of characteristic roots
Used byCharacter vanishing from coprimality and a strict norm bound

TheoremCharacter vanishing from coprimality and a strict norm bound#✓fully proved

Let \(G\) be a finite group, let \(\rho\) be an irreducible representation of \(G\) on a nonzero finite-dimensional complex vector space \(V\), with character \(\chi\), and let \(g \in G\). If the size of the conjugacy class of \(g\) is coprime to \(\dim V\) and \(|\chi(g)| < \dim V\), then \(\chi(g) = 0\).

theorem char_eq_zero_of_coprime_of_norm_lt {V : Type*} [AddCommGroup V]
    [Module ℂ V] [FiniteDimensional ℂ V] [Nontrivial V]
    (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] (g : G)
    (hcop : Nat.Coprime (conjClass g).card (Module.finrank ℂ V))
    (hlt : ‖ρ.character g‖ < Module.finrank ℂ V) :
    ρ.character g = 0
Sources
  • Bielefeld Theorem 5, norm step.
Uses 10 · Used by 1
Statement usesConjugacy class
Proof usesIntegrality of the normalized character value at a coprime class · Character values lie in a cyclotomic field · Characteristic roots are killed by the order of the element · Number of characteristic roots of a representation matrix · Characteristic roots as elements of the cyclotomic field · Cyclotomic subfield of \(\mathbb{C}\) · The zeroth cyclotomic field is \(\mathbb{Q}\) · The \(m\)-th cyclotomic field is a splitting field of \(X^m - 1\) · Field embeddings applied to character values
Used byBurnside's vanishing theorem for coprime class sizes

TheoremBurnside's vanishing theorem for coprime class sizes#✓fully proved

Let \(G\) be a finite group, let \(\rho\) be an irreducible representation of \(G\) on a nonzero finite-dimensional complex vector space \(V\), with character \(\chi\), and let \(g \in G\). If the size of the conjugacy class of \(g\) is coprime to \(\dim V\), then \(|\chi(g)| = \dim V\) or \(\chi(g) = 0\).

Since \(\chi(1) = \dim V\), the first alternative says that \(g\) lies in the center \(Z(\chi)\) of \(\chi\), the set of \(h \in G\) with \(|\chi(h)| = \chi(1)\).

theorem burnside_coprime_vanish {V : Type*} [AddCommGroup V]
    [Module ℂ V] [FiniteDimensional ℂ V] [Nontrivial V]
    (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] (g : G)
    (hcop : Nat.Coprime (conjClass g).card (Module.finrank ℂ V)) :
    ‖ρ.character g‖ = Module.finrank ℂ V ∨ ρ.character g = 0
Sources
  • Bielefeld Theorem 5.
Uses 5 · Used by 1
Statement usesConjugacy class
Proof usesCharacter vanishing from coprimality and a strict norm bound · Character value as the sum of characteristic roots · Eigenvalues of a finite group representation have modulus one · Number of characteristic roots of a representation matrix
Used byNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size

TheoremSelf-orthogonality of an irreducible character#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space, with character \(\chi\). Then \(\sum_{g \in G} \chi(g)\chi(g^{-1}) = |G|\).

theorem self_pair_sum {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] :
    ∑ g : G, ρ.character g * ρ.character g⁻¹ = (Nat.card G : ℂ)
Used by 1
Used byDegrees of irreducible representations divide the group order

TheoremSplitting a sum over conjugacy classes#✓fully proved

For a finite group \(G\) and every function \(f : G \to \mathbb{C}\), \(\sum_{g \in G} f(g) = \sum_{l} \sum_{x \in l} f(x)\), where \(l\) runs over the conjugacy classes of \(G\).

theorem sum_over_classes (f : G → ℂ) :
    ∑ g : G, f g
      = ∑ l : ConjClasses G, ∑ x ∈ (ConjClasses.carrier l).toFinset, f x
Used by 1
Used byDegrees of irreducible representations divide the group order

TheoremMembers of a conjugacy class are conjugate to its representative#✓fully proved

Let \(l\) be a conjugacy class of a finite group \(G\) and \(g_l\) its chosen representative. For every \(x \in l\) there is \(c \in G\) with \(c x c^{-1} = g_l\).

theorem conj_to_rep (l : ConjClasses G) (x : G)
    (hx : x ∈ (ConjClasses.carrier l).toFinset) :
    ∃ c : G, c * x * c⁻¹ = classRep l
Uses 1 · Used by 2
Statement usesChosen representative of a conjugacy class
Used byCharacters are constant on conjugacy classes · Characters at inverses are constant on conjugacy classes

TheoremCharacters are constant on conjugacy classes#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space, with character \(\chi\), and let \(g_l\) be the chosen representative of a conjugacy class \(l\) of \(G\). Then \(\chi(x) = \chi(g_l)\) for every \(x \in l\).

theorem char_eq_of_mem_carrier {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (l : ConjClasses G)
    (x : G) (hx : x ∈ (ConjClasses.carrier l).toFinset) :
    ρ.character x = ρ.character (classRep l)
Uses 2 · Used by 1
Statement usesChosen representative of a conjugacy class
Proof usesMembers of a conjugacy class are conjugate to its representative
Used byContribution of a conjugacy class to the self-pairing sum

TheoremCharacters at inverses are constant on conjugacy classes#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space, with character \(\chi\), and let \(g_l\) be the chosen representative of a conjugacy class \(l\) of \(G\). Then \(\chi(x^{-1}) = \chi(g_l^{-1})\) for every \(x \in l\).

theorem char_inv_eq_of_mem_carrier {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (l : ConjClasses G)
    (x : G) (hx : x ∈ (ConjClasses.carrier l).toFinset) :
    ρ.character x⁻¹ = ρ.character (classRep l)⁻¹
Uses 2 · Used by 1
Statement usesChosen representative of a conjugacy class
Proof usesMembers of a conjugacy class are conjugate to its representative
Used byContribution of a conjugacy class to the self-pairing sum

TheoremContribution of a conjugacy class to the self-pairing sum#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), with character \(\chi\). For a conjugacy class \(l\) of \(G\), let \(g_l\) be its chosen representative and \(\omega(l)\) the central scalar of \(l\), the scalar by which the class sum of \(l\) acts on \(V\). Then \(\sum_{x \in l} \chi(x)\chi(x^{-1}) = (\dim_{\mathbb{C}} V)\,\omega(l)\,\chi(g_l^{-1})\).

theorem class_inner_sum {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] (l : ConjClasses G) :
    ∑ x ∈ (ConjClasses.carrier l).toFinset, ρ.character x * ρ.character x⁻¹
      = (Module.finrank ℂ V : ℂ)
        * (centralScalar ρ l * ρ.character (classRep l)⁻¹)
Uses 5 · Used by 1
Statement usesCentral scalar of a conjugacy class · Chosen representative of a conjugacy class
Proof usesTrace formula for central scalars · Characters are constant on conjugacy classes · Characters at inverses are constant on conjugacy classes
Used byDegrees of irreducible representations divide the group order

TheoremDegrees of irreducible representations divide the group order#✓fully proved

Let \(\rho\) be an irreducible representation of a finite group \(G\) on a nonzero finite-dimensional complex vector space \(V\). Then \(\dim_{\mathbb{C}} V\) divides \(|G|\).

theorem degree_dvd_card {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] :
    Module.finrank ℂ V ∣ Fintype.card G
Sources
  • Bielefeld Corollary 2.
Uses 7
Proof usesCentral scalar of a conjugacy class · Central scalars are algebraic integers · Character values are algebraic integers · Chosen representative of a conjugacy class · Contribution of a conjugacy class to the self-pairing sum · Self-orthogonality of an irreducible character · Splitting a sum over conjugacy classes

TheoremCharacters of full absolute value have equal eigenvalues#✓fully proved

Let \(G\) be a finite group, \(V\) a nonzero finite-dimensional complex vector space and \(\rho\) an irreducible representation of \(G\) on \(V\) with character \(\chi\). If \(g \in G\) satisfies \(|\chi(g)| = \dim V\), then any two roots of the characteristic polynomial of \(\rho(g)\) are equal.

theorem all_roots_eq_of_norm_eq {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] [Finite G] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] (g : G)
    (h : ‖ρ.character g‖ = Module.finrank ℂ V) :
    ∀ μ₁ ∈ (ρ g).charpoly.roots, ∀ μ₂ ∈ (ρ g).charpoly.roots, μ₁ = μ₂
Uses 4 · Used by 1
Proof usesStrict triangle inequality for unit complex numbers, multiset form · Character value as the sum of characteristic roots · Eigenvalues of a finite group representation have modulus one · Number of characteristic roots of a representation matrix
Used byNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size

TheoremElements with a single eigenvalue act as scalars#✓fully proved

Let \(G\) be a finite group, \(V\) a nonzero finite-dimensional complex vector space, \(\rho\) a representation of \(G\) on \(V\), \(g \in G\) and \(\mu_0 \in \mathbb{C}\). If every root of the characteristic polynomial of \(\rho(g)\) equals \(\mu_0\), then \(\rho(g) = \mu_0 \cdot \mathrm{id}_V\).

theorem eq_smul_one_of_all_roots_eq {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] [Finite G] (ρ : Representation ℂ G V) (g : G)
    (μ₀ : ℂ) (hall : ∀ μ ∈ (ρ g).charpoly.roots, μ = μ₀) :
    (ρ g : Module.End ℂ V) = μ₀ • 1
Uses 1 · Used by 1
Proof usesNumber of characteristic roots of a representation matrix
Used byNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size

DefinitionScalar center of a representation#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a nonzero complex vector space \(V\). The scalar center of \(\rho\) is the subgroup of \(G\) consisting of the elements \(g\) such that \(\rho(g) = c \cdot \mathrm{id}_V\) for some \(c \in \mathbb{C}\).

BurnsidePaqb.charCenter · 23 lines 
noncomputable def charCenter {V : Type*} [AddCommGroup V] [Module ℂ V] [Nontrivial V]
    (ρ : Representation ℂ G V) : Subgroup G where
  carrier := { g | ∃ c : ℂ, (ρ g : Module.End ℂ V) = c • 1 }
  one_mem' := ⟨1, by rw [map_one, one_smul]⟩
  mul_mem' := by
    intro a b ha hb
    obtain ⟨c₁, hc₁⟩ := ha
    obtain ⟨c₂, hc₂⟩ := hb
    refine ⟨c₁ * c₂, ?_⟩
    rw [map_mul, hc₁, hc₂, smul_mul_assoc, one_mul, smul_smul]
  inv_mem' := by
    intro g hg
    obtain ⟨c, hc⟩ := hg
    have key : (ρ g⁻¹ : Module.End ℂ V) * (ρ g : Module.End ℂ V) = 1 := by
      rw [← map_mul, inv_mul_cancel, map_one]
    rw [hc, mul_smul_comm, mul_one] at key
    have hc0 : c ≠ 0 := by
      intro hz
      rw [hz, zero_smul] at key
      exact one_ne_zero key.symm
    refine ⟨c⁻¹, ?_⟩
    have hsm := congrArg (c⁻¹ • ·) key
    rwa [smul_smul, inv_mul_cancel₀ hc0, one_smul] at hsm
Used by 6
Used byThe scalar center of a nonlinear irreducible representation is proper · Nonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size · Elements of the scalar center act by scalars · Membership in the scalar center · Elements acting by a scalar lie in the scalar center · Elements of the scalar center have character of full absolute value

TheoremMembership in the scalar center#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a nonzero complex vector space \(V\). An element \(g \in G\) lies in the scalar center of \(\rho\) if and only if \(\rho(g) = c \cdot \mathrm{id}_V\) for some \(c \in \mathbb{C}\).

theorem mem_charCenter_iff {V : Type*} [AddCommGroup V] [Module ℂ V] [Nontrivial V]
    (ρ : Representation ℂ G V) (g : G) :
    g ∈ charCenter ρ ↔ ∃ c : ℂ, (ρ g : Module.End ℂ V) = c • 1
Uses 1
Statement usesScalar center of a representation

TheoremElements acting by a scalar lie in the scalar center#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a nonzero complex vector space \(V\). If \(g \in G\) and \(c \in \mathbb{C}\) satisfy \(\rho(g) = c \cdot \mathrm{id}_V\), then \(g\) lies in the scalar center of \(\rho\).

theorem mem_charCenter_of_eq_smul {V : Type*} [AddCommGroup V] [Module ℂ V]
    [Nontrivial V] (ρ : Representation ℂ G V) (g : G) (c : ℂ)
    (hc : (ρ g : Module.End ℂ V) = c • 1) : g ∈ charCenter ρ
Uses 1 · Used by 1
Statement usesScalar center of a representation
Used byNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size

TheoremElements of the scalar center act by scalars#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a nonzero complex vector space \(V\). If \(g\) lies in the scalar center of \(\rho\), then there is \(c \in \mathbb{C}\) with \(\rho(g) = c \cdot \mathrm{id}_V\).

theorem exists_eq_smul_of_mem_charCenter {V : Type*} [AddCommGroup V] [Module ℂ V]
    [Nontrivial V] (ρ : Representation ℂ G V) (g : G) (h : g ∈ charCenter ρ) :
    ∃ c : ℂ, (ρ g : Module.End ℂ V) = c • 1
Uses 1
Statement usesScalar center of a representation

TheoremThe scalar center of a nonlinear irreducible representation is proper#✓fully proved

Let \(\rho\) be an irreducible representation of a group \(G\) on a finite-dimensional complex vector space \(V\) with \(\dim V > 1\). Then the scalar center of \(\rho\) is a proper subgroup of \(G\).

theorem charCenter_proper_of_nonlinear {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] (h : 1 < Module.finrank ℂ V) :
    charCenter ρ ≠ ⊤
Uses 1 · Used by 1
Statement usesScalar center of a representation
Used byNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size

TheoremElements of the scalar center have character of full absolute value#✓fully proved

Let \(G\) be a finite group, \(V\) a nonzero finite-dimensional complex vector space and \(\rho\) a representation of \(G\) on \(V\) with character \(\chi\). If \(g\) lies in the scalar center of \(\rho\), then \(|\chi(g)| = \dim V\).

theorem norm_eq_of_mem_charCenter {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] [Finite G] (ρ : Representation ℂ G V)
    (g : G) (h : g ∈ charCenter ρ) :
    ‖ρ.character g‖ = Module.finrank ℂ V
Uses 1
Statement usesScalar center of a representation

TheoremAn algebraic integer cannot solve \(1 + p\beta = 0\) for a prime \(p\)#✓fully proved

Let \(p\) be a prime number. There is no algebraic integer \(\beta \in \mathbb{C}\) with \(1 + p\beta = 0\), since such a \(\beta\) would make \(-1/p\) an algebraic integer.

theorem false_of_one_add_prime_mul_isIntegral {p : ℕ} (hp : p.Prime)
    {β : ℂ} (hβ : IsIntegral ℤ β) (h : 1 + (p : ℂ) * β = 0) : False
Used by 1
Used byA simple group with a prime-power conjugacy class has prime order

TheoremOne-dimensional representations act by their character#✓fully proved

Let \(\rho\) be a representation of a group \(G\) on a complex vector space \(V\) of dimension \(1\), and let \(\chi\) be the character of \(\rho\). Then for every \(g \in G\) the operator \(\rho(g)\) is multiplication by the scalar \(\chi(g)\), that is, \(\rho(g) = \chi(g) \cdot \mathrm{id}_V\).

theorem eq_smul_one_of_finrank_one {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (ρ : Representation ℂ G V)
    (hd : Module.finrank ℂ V = 1) (g : G) :
    ρ g = ρ.character g • 1
Used by 1
Used byA linear character as a homomorphism to \(\mathbb{C}^\times\)

DefinitionA linear character as a homomorphism to \(\mathbb{C}^\times\)#✓fully proved

Let \(G\) be a finite group and let \(\rho\) be a representation of \(G\) on a complex vector space \(V\) of dimension \(1\), with character \(\chi\). This is the group homomorphism from \(G\) to the multiplicative group \(\mathbb{C}^\times\) of nonzero complex numbers that sends \(g\) to \(\chi(g)\).

BurnsidePaqb.linearCharHom · 18 lines 
noncomputable def linearCharHom {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    (hd : Module.finrank ℂ V = 1) : G →* ℂˣ :=
  MonoidHom.toHomUnits
    { toFun := fun g => ρ.character g
      map_one' := by rw [Representation.char_one, hd]; simp
      map_mul' := fun g h => by
        have h1 := eq_smul_one_of_finrank_one ρ hd g
        have h2 := eq_smul_one_of_finrank_one ρ hd h
        have h3 := eq_smul_one_of_finrank_one ρ hd (g * h)
        have hmul : ρ (g * h) = ρ g * ρ h := map_mul ρ g h
        have htr : ρ.character (g * h)
            = ρ.character g * ρ.character h := by
          have e : (ρ.character (g * h)) • (1 : Module.End ℂ V)
              = (ρ.character g * ρ.character h) • 1 := by
            rw [← h3, hmul, h1, h2, smul_mul_smul, one_mul]
          exact smul_left_injective ℂ (one_ne_zero : (1 : Module.End ℂ V) ≠ 0) e
        exact htr }
Uses 1 · Used by 1
Statement usesOne-dimensional representations act by their character
Used byA simple group with a nontrivial linear character has prime order

TheoremA simple group with a nontrivial linear character has prime order#✓fully proved

Let \(G\) be a finite simple group and let \(\rho\) be a representation of \(G\) on a complex vector space \(V\) of dimension \(1\). If the character of \(\rho\) is not the constant function \(1\), then the order of \(G\) is a prime number.

theorem card_eq_prime_of_nontrivial_linear [IsSimpleGroup G]
    {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    (hd : Module.finrank ℂ V = 1) (hne : ρ.character ≠ 1) :
    ∃ r : ℕ, r.Prime ∧ Fintype.card G = r
Uses 1 · Used by 1
Proof usesA linear character as a homomorphism to \(\mathbb{C}^\times\)
Used byA simple group with a prime-power conjugacy class has prime order

TheoremNonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size#✓fully proved

Nonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size. Let \(G\) be a finite simple group, let \(\rho\) be an irreducible representation of \(G\) on a finite-dimensional complex vector space \(V\) of dimension \(d > 1\), and let \(\chi\) be the character of \(\rho\). If \(g \ne 1\) is an element of \(G\) whose conjugacy class has size coprime to \(d\), then \(\chi(g) = 0\).

theorem char_zero_of_nonlinear_of_coprime [IsSimpleGroup G]
    {V : Type*} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] [Nontrivial V] (ρ : Representation ℂ G V)
    [Representation.IsIrreducible ρ] (g : G) (hne1 : g ≠ 1)
    (hd : 1 < Module.finrank ℂ V)
    (hcop : Nat.Coprime (conjClass g).card (Module.finrank ℂ V)) :
    ρ.character g = 0
Uses 8 · Used by 1
Statement usesConjugacy class
Proof usesCharacters of full absolute value have equal eigenvalues · Burnside's vanishing theorem for coprime class sizes · Scalar center of a representation · The scalar center of a nonlinear irreducible representation is proper · Number of characteristic roots of a representation matrix · Elements with a single eigenvalue act as scalars · Elements acting by a scalar lie in the scalar center
Used byA simple group with a prime-power conjugacy class has prime order

TheoremA simple group with a prime-power conjugacy class has prime order#✓fully proved

Let \(G\) be a finite simple group and let \(g \ne 1\) be an element of \(G\) whose conjugacy class has size \(r^k\) for some prime \(r\) and some \(k \ge 1\). Then the order of \(G\) is a prime number.

theorem cor6_of_prime_pow_class {G : Type} [Group G] [Fintype G] [IsSimpleGroup G]
    (g : G) (hg1 : g ≠ 1) (hpp : IsPrimePow (conjClass g).card) :
    ∃ r : ℕ, r.Prime ∧ Fintype.card G = r
Sources
  • Bielefeld Corollary 6.
Uses 16 · Used by 1
Statement usesConjugacy class
Proof usesIsomorphism classes of simple representations · Character of an isomorphism class · Character of a class via its chosen representative · Characters determine irreducible representations · Character value at the identity · Character of the trivial representation · Chosen representative of an isomorphism class · The trivial irreducible class · Bound on the number of irreducible representations · A simple group with a nontrivial linear character has prime order · Nonlinear irreducible characters of a simple group vanish on nonidentity classes of coprime size · Character values are algebraic integers · An algebraic integer cannot solve \(1 + p\beta = 0\) for a prime \(p\) · Simple finite-dimensional complex representations of a finite group are irreducible · Column orthogonality at the identity
Used byBurnside's \(p^a q^b\) theorem in the lowest universe

TheoremDivisors of \(p^a q^b\)#✓fully proved

Let \(p\) and \(q\) be primes and let \(a\) and \(b\) be natural numbers. Every natural number \(d\) dividing \(p^a q^b\) has the form \(d = p^{a'} q^{b'}\) for some natural numbers \(a'\) and \(b'\).

theorem eq_prime_pow_mul_of_dvd {p q a b d : ℕ} (hp : p.Prime)
    (hq : q.Prime) (hdvd : d ∣ p ^ a * q ^ b) :
    ∃ a' b', d = p ^ a' * q ^ b'
Used by 1
Used byBurnside's \(p^a q^b\) theorem from the prime-power class corollary

TheoremGroups of prime order are solvable#✓fully proved

Every finite group whose order is a prime number is solvable.

theorem isSolvable_of_prime_card (r : ℕ) (hr : r.Prime)
    (hcard : Fintype.card G = r) : Group.IsSolvable G
Used by 1
Used byBurnside's \(p^a q^b\) theorem from the prime-power class corollary

TheoremBurnside's \(p^a q^b\) theorem from the prime-power class corollary#✓fully proved

Suppose that every finite simple group \(H\) having an element \(h \ne 1\) whose conjugacy class has size \(r^k\) for some prime \(r\) and some \(k \ge 1\) has prime order. Then for all primes \(p\) and \(q\) and all natural numbers \(a\) and \(b\), every finite group \(G\) of order \(p^a q^b\) is solvable.

theorem burnside_paqb_of_simple_prime
    (C6 : ∀ {H : Type u} [Group H] [Fintype H], IsSimpleGroup H →
      (∃ g : H, g ≠ 1 ∧ IsPrimePow (conjClass g).card) →
      ∃ r : ℕ, r.Prime ∧ Fintype.card H = r)
    (p q : ℕ) (a b : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q)
    (hcard : Fintype.card G = p ^ a * q ^ b) : Group.IsSolvable G
Sources
  • Bielefeld Theorem 7.
Uses 5 · Used by 1
Statement usesConjugacy class
Proof usesConjugacy classes are closed under conjugation · Divisors of \(p^a q^b\) · A nontrivial element whose class size is a power of \(p\) · Groups of prime order are solvable
Used byBurnside's \(p^a q^b\) theorem in the lowest universe

TheoremBurnside's \(p^a q^b\) theorem in the lowest universe#✓fully proved

Let \(G\) be a finite group whose underlying type lies in the lowest type universe, let \(p\) and \(q\) be primes and let \(a\) and \(b\) be natural numbers. If \(G\) has order \(p^a q^b\), then \(G\) is solvable.

theorem burnside_paqb_zero {G : Type} [Group G] [Fintype G]
    (p q : ℕ) (a b : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q)
    (hcard : Fintype.card G = p ^ a * q ^ b) : Group.IsSolvable G
Uses 3 · Used by 1
Proof usesBurnside's \(p^a q^b\) theorem from the prime-power class corollary · Conjugacy class · A simple group with a prime-power conjugacy class has prime order
Used byBurnside's \(p^a q^b\) theorem

TheoremBurnside's \(p^a q^b\) theorem#✓fully proved

Let \(G\) be a finite group, let \(p\) and \(q\) be primes and let \(a\) and \(b\) be natural numbers. If \(G\) has order \(p^a q^b\), then \(G\) is solvable.

theorem burnside_paqb {G : Type*} [Group G] [Fintype G]
    (p q a b : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q)
    (hcard : Fintype.card G = p ^ a * q ^ b) : Group.IsSolvable G
Uses 1
Proof usesBurnside's \(p^a q^b\) theorem in the lowest universe
99 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.