Brauer's splitting field theorem

brauer_splitting_field

Submitter: Kim Morrison.

Notes: For a finite group G of exponent n, the cyclotomic field ℚ(ζₙ) is a splitting field for G: every finite-dimensional complex representation ρ of G descends to ℚ(ζₙ). Concretely, there exists an embedding φ : CyclotomicField n ℚ →+* ℂ, a ℚ(ζₙ)-representation (W, σ) of G, and a ℂ-linear G-equivariant isomorphism ℂ ⊗[ℚ(ζₙ)] W ≃ V (with ℂ viewed as a ℚ(ζₙ)-algebra via φ). The G-equivariance is expressed against the base-changed action `(σ g).baseChange ℂ`. Strictly stronger than the character-value statement `brauer_character_in_cyclotomic`, which follows by taking traces and is in fact elementary.

Source: 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.

Informal solution: Pick any embedding φ : ℚ(ζₙ) ↪ ℂ. By Maschke's theorem ρ decomposes as a direct sum of irreducible complex representations, so it suffices to descend each irreducible ρᵢ separately. Brauer's induction theorem expresses the character of each ρᵢ as a ℤ-combination of characters induced from one-dimensional characters of elementary subgroups; these one-dimensional characters take values in ℚ(ζₙ), so each induced representation is realised on a ℚ(ζₙ)-module. The Schur index of each ρᵢ over ℚ(ζₙ) is therefore 1, meaning ρᵢ itself descends to ℚ(ζₙ): there exists a ℚ(ζₙ)[G]-module Wᵢ with ℂ ⊗_{ℚ(ζₙ)} Wᵢ ≃ Vᵢ as ℂ[G]-modules. Assemble the Wᵢ into W and the isomorphisms into f to conclude.

theorem declaration uses `sorry`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) := byG:Typeinst✝⁴:Group Ginst✝³:Fintype GV:Typeinst✝²:AddCommGroup Vinst✝¹:Module ℂ Vinst✝:FiniteDimensional ℂ Vρ:Representation ℂ G V⊢ ∃ φ W x x_1 σ f,
  ∀ (g : G) (x_2 : ℂ ⊗[CyclotomicField (Monoid.exponent G) ℚ] W), f ((LinearMap.baseChange ℂ (σ g)) x_2) = (ρ g) (f x_2)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.