Brauer's splitting field theorem

TheoremCharacter values of a finite group lie in a cyclotomic field#●ready to prove

Let \(G\) be a finite group of exponent \(n\), and let \(\mathbb{Q}(\zeta_n)\) be the \(n\)-th cyclotomic field. There is a ring homomorphism \(\varphi \colon \mathbb{Q}(\zeta_n) \to \mathbb{C}\) such that for every finite-dimensional complex representation \(\rho\) of \(G\) on a vector space \(V\) and every \(g \in G\), the trace of \(\rho(g)\) lies in the image of \(\varphi\).

public theorem_wanted brauer_character_in_cyclotomic
    (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range

Sources

• R. Brauer, On the representation of a group of order g in the field of g-th roots of unity, Amer. J. Math. 67 (1945). Problem brauer_character_in_cyclotomic of the lean-eval benchmark.

TheoremBrauer's splitting field theorem#●ready to prove

Let \(G\) be a finite group of exponent \(n\), let \(K = \mathbb{Q}(\zeta_n)\) be the \(n\)-th cyclotomic field, and let \(\rho\) be a representation of \(G\) on a finite-dimensional complex vector space \(V\). Then there are a ring homomorphism \(\varphi \colon K \to \mathbb{C}\), a \(K\)-vector space \(W\) with a representation \(\sigma\) of \(G\) on \(W\), and a \(\mathbb{C}\)-linear isomorphism \(f \colon \mathbb{C} \otimes_K W \to V\), where \(\mathbb{C}\) is regarded as a \(K\)-algebra via \(\varphi\), such that \(f((\mathrm{id}_{\mathbb{C}} \otimes \sigma(g))(x)) = \rho(g)(f(x))\) for all \(g \in G\) and all \(x \in \mathbb{C} \otimes_K W\).

public theorem_wanted brauer_splitting_field
    (G : Type) [Group G] [Fintype G]
    (V : Type) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) :
    ∃ (φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ)
      (W : Type) (_ : AddCommGroup W)
      (_ : Module (CyclotomicField (Monoid.exponent G) ℚ) W)
      (σ : Representation (CyclotomicField (Monoid.exponent G) ℚ) G W),
      letI : Algebra (CyclotomicField (Monoid.exponent G) ℚ) ℂ := φ.toAlgebra
      ∃ (f : (ℂ ⊗[CyclotomicField (Monoid.exponent G) ℚ] W) ≃ₗ[ℂ] V),
        ∀ (g : G) (x : ℂ ⊗[CyclotomicField (Monoid.exponent G) ℚ] W),
          f ((σ g).baseChange ℂ x) = ρ g (f x)

Sources

• R. Brauer, On the representation of a group of order g in the field of g-th roots of unity, Amer. J. Math. 67 (1945), 461–471. Problem brauer_splitting_field of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.