The Frobenius-Schur indicator of a representation realizable over the reals

This file proves the direction of the Frobenius-Schur orthogonality criterion that goes from a real form to the indicator: an irreducible representation with a real form is orthogonal, ν₂(ρ) = 1. The real-form vocabulary itself -- Representation.IsRealForm and Representation.IsRealizableOverReal -- is in TauCeti.RepresentationTheory.RealForm and needs none of the Frobenius-Schur layer.

The route is the one the trichotomy already asks for, an invariant symmetric form. A representation of a finite group on a nontrivial finite-dimensional real space carries a nonzero invariant symmetric form, obtained by summing the coordinate dot product of a basis over the conjugates (Representation.exists_isInvariantForm_isSymm_ne_zero, in TauCeti.RepresentationTheory.InvariantForm.SumOfConjugates); both hypotheses are free here, because irreducibility over a finite group makes V nontrivial and finite-dimensional and the real form passes each of them to W. A real form then transports the form to a nonzero invariant symmetric form on V (Representation.IsRealForm.exists_isInvariantForm_isSymm_ne_zero), and TauCeti.Representation.frobeniusSchurIndicator_eq_one_of_isSymm reads off the indicator. Finiteness of G is used twice over: the indicator itself and the trichotomy consumed here are stated for a finite group, and the summing step needs it again to build the invariant form. The real-form vocabulary is the part that needs none of it.

The converse -- that an irreducible representation with ν₂(ρ) = 1 is realizable over ℝ -- is a strictly stronger statement than the existence of an invariant symmetric form supplied by TauCeti.Representation.frobeniusSchurIndicator_eq_one_iff: passing from the form to a real structure needs an invariant Hermitian inner product as well, and the antilinear involution built from the two of them. It is proved separately, in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Realizability.lean, on top of the real-structure vocabulary of TauCeti/RepresentationTheory/RealForm.lean: Representation.IsRealStructure is such an involution, its fixed points are a real form (Representation.IsRealStructure.isRealForm), and Representation.isRealizableOverReal_iff_exists_isRealStructure turns one into realizability over ℝ.

Main results

• Representation.IsRealForm.frobeniusSchurIndicator_eq_one and Representation.frobeniusSchurIndicator_eq_one_of_isRealizableOverReal: an irreducible representation realizable over ℝ has Frobenius-Schur indicator 1.

References

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 4.

theorem Representation.IsRealForm.frobeniusSchurIndicator_eq_one {G : Type u_1} [Group G] [Fintype G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} [ρ.IsIrreducible] (h : ρ.IsRealForm σ) : TauCeti.Representation.frobeniusSchurIndicator ρ = 1

An irreducible representation with a real form is orthogonal. Summing the dot product of a basis over the conjugates produces a nonzero invariant symmetric form on the real side, and transporting it along the real form makes the complex representation carry one too, which is exactly the orthogonal case of the Frobenius-Schur trichotomy.

No finiteness is assumed of the real form: irreducibility over a finite group already makes V finite-dimensional (Mathlib's instance on ρ.asModule, read back on V along ρ.asModuleEquiv), which W inherits (Representation.IsRealForm.finiteDimensional_iff), and a real form has the same dimension as the representation it is a form of (Representation.IsRealForm.finrank_eq), so W is nontrivial too.

theorem Representation.frobeniusSchurIndicator_eq_one_of_isRealizableOverReal {G : Type u_1} [Group G] [Fintype G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [ρ.IsIrreducible] (h : ρ.IsRealizableOverReal) : TauCeti.Representation.frobeniusSchurIndicator ρ = 1

An irreducible representation realizable over ℝ has Frobenius-Schur indicator 1. This is the "realizable" half of the orthogonality criterion; the converse, that indicator 1 produces a real form, is Representation.isRealizableOverReal_of_frobeniusSchurIndicator_eq_one.