The Frobenius-Schur indicator of a compact group

For a finite-dimensional continuous representation π of a compact group G, the Frobenius-Schur indicator is the Haar average of the character over squares,

ν₂(π) = ∫_G χ_π(g²) dμ,

with μ the normalized Haar measure of TauCeti/RepresentationTheory/Compact/Haar.lean. It is the compact-group form of the finite average |G|⁻¹ ∑_g χ(g²) built in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Basic.lean; the integral replaces the average and nothing else changes in the statement.

What the indicator computes is the signed difference of the two square characters. Over any field χ_{Sym²}(g) - χ_{Λ²}(g) = χ(g²) (Representation.char_symmetricSquare_sub_char_exteriorSquare), so integrating that identity gives

ν₂(π) = ∫_G χ_{Sym²π} - ∫_G χ_{Λ²π},

and the companion identity χ(g)² = χ_{Sym²}(g) + χ_{Λ²}(g) gives the two integrals separately in terms of ν₂(π) and ∫_G χ_π². Those two integrals are the (complexified) dimensions of the invariants of the two squares once the projection onto invariants built from the Haar averaging operator is available; here only the character-level identities are proved, which is what makes them independent of that development.

The two square characters are not, a priori, characters of continuous representations: the symmetric and exterior square of a continuous representation carry a continuous action, but that is not what is used. The closed formulas χ_{Sym²}(g) = ½(χ(g)² + χ(g²)) and χ_{Λ²}(g) = ½(χ(g)² - χ(g²)), valid because 2 ≠ 0, exhibit both as continuous functions of g directly, and that is all integration needs; that continuity is TauCeti/RepresentationTheory/Continuous/Square/Character.lean, which needs neither a group nor a measure, and only the integrability it yields is proved here.

For a unitary representation the indicator is real (ContRepresentation.conj_frobeniusSchurIndicator): conjugating the character inverts its argument, (g²)⁻¹ = (g⁻¹)², and Haar measure on a compact group is inversion invariant. Its modulus is at most dim V. That it takes only the values 1, 0, -1 on an irreducible is the reality trichotomy, which is not proved here but in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Trichotomy.lean; the reading of those three values as invariant bilinear forms is TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantForm.lean.

Main definitions

• ContRepresentation.frobeniusSchurIndicator: ν₂(π) = ∫_G χ_π(g²) dμ.

Main statements

• ContRepresentation.frobeniusSchurIndicator_eq_of_equiv: the indicator depends only on the equivalence class of the representation.
• ContRepresentation.frobeniusSchurIndicator_eq_sub_integral: the indicator is the difference of the two square-character integrals, ν₂(π) = ∫ χ_{Sym²π} - ∫ χ_{Λ²π}.
• ContRepresentation.integral_character_sq: the two square-character integrals add up to ∫ χ_π², so together with the previous statement they determine both: ContRepresentation.integral_character_symmetricPower_two and ContRepresentation.integral_character_exteriorPower_two are the resulting closed forms ½(∫ χ_π² ± ν₂(π)).
• ContRepresentation.conj_frobeniusSchurIndicator and ContRepresentation.im_frobeniusSchurIndicator: the indicator of a unitary representation is real.
• ContRepresentation.norm_frobeniusSchurIndicator_le: it has modulus at most dim V.
• ContRepresentation.frobeniusSchurIndicator_trivial: the indicator of the trivial representation is its dimension, in particular 1 on the line.

Implementation notes

The continuity hypothesis hπ : Continuous π is the one ContRepresentation.character already carries: ContRepresentation bundles continuous action operators without asking that the map to them be continuous. Since it is a Prop argument, two indicators built from different continuity proofs are equal by proof irrelevance.

Everything below is declared in the root ContRepresentation namespace rather than in TauCeti.ContRepresentation, so that π.frobeniusSchurIndicator hπ elaborates: ContRepresentation is Mathlib's type, and a namespace for it nested inside TauCeti does not support dot notation. The ambient TauCeti names this file consumes, such as TauCeti.haarProb and TauCeti.integrable_continuousMap, are brought in by open. The character and its formulas are methods in ContRepresentation.

The scalars are ℂ: the symmetric- and exterior-power representations of TauCeti/RepresentationTheory/SymmetricPower.lean and TauCeti/RepresentationTheory/ExteriorPower.lean, whose characters the square identities below speak of, are built over a base ring in Type, so a general RCLike field in an arbitrary universe would not even let the statements be formed.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and Bröcker-tom Dieck, Representations of Compact Lie Groups, Chapter II.

theorem ContRepresentation.integrable_character_mul_self {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : MeasureTheory.Integrable (fun (g : G) => (π.character hπ) (g * g)) (TauCeti.haarProb G)

The character read along the squaring map is integrable against normalized Haar measure, so the Frobenius-Schur indicator below is a genuine average and not the Bochner integral's junk value.

noncomputable def ContRepresentation.frobeniusSchurIndicator {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : ℂ

The Frobenius-Schur indicator of a finite-dimensional continuous representation of a compact group: the Haar average ν₂(π) = ∫_G χ_π(g²) dμ of the character over squares.

Equations

• π.frobeniusSchurIndicator hπ = ∫ (g : G), (π.character hπ) (g * g) ∂TauCeti.haarProb G

theorem ContRepresentation.frobeniusSchurIndicator_def {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : π.frobeniusSchurIndicator hπ = ∫ (g : G), (π.character hπ) (g * g) ∂TauCeti.haarProb G

The defining integral of the Frobenius-Schur indicator.

theorem ContRepresentation.frobeniusSchurIndicator_eq_of_equiv {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) {W : Type u_3} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (σ : ContRepresentation ℂ G W) (hσ : Continuous ⇑σ) (φ : (toRepresentation ℂ G V π).Equiv (toRepresentation ℂ G W σ)) : π.frobeniusSchurIndicator hπ = σ.frobeniusSchurIndicator hσ

Equivalent representations have the same Frobenius-Schur indicator, since they have the same character (Representation.char_iso). The two continuity witnesses are unrelated: the indicator reads only the underlying representation, so nothing links them.

@[simp]

theorem ContRepresentation.frobeniusSchurIndicator_trivial {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] : (trivial ℂ G V).frobeniusSchurIndicator ⋯ = ↑(Module.finrank ℂ V)

The Frobenius-Schur indicator of the trivial representation is its dimension: every character value is dim V, and Haar measure is normalized. On the line this is ν₂ = 1.

The two square characters

Over any field the difference of the symmetric-square and exterior-square characters is the character at the square, and their sum is the square of the character. Integrating both identities expresses the two square-character integrals through ν₂(π) and ∫ χ_π².

theorem ContRepresentation.integrable_character_symmetricPower_two {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : MeasureTheory.Integrable (fun (g : G) => ((toRepresentation ℂ G V π).symmetricPower 2).character g) (TauCeti.haarProb G)

The symmetric-square character is integrable against normalized Haar measure.

theorem ContRepresentation.integrable_character_exteriorPower_two {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : MeasureTheory.Integrable (fun (g : G) => ((toRepresentation ℂ G V π).exteriorPower 2).character g) (TauCeti.haarProb G)

The exterior-square character is integrable against normalized Haar measure.

theorem ContRepresentation.frobeniusSchurIndicator_eq_sub_integral {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : π.frobeniusSchurIndicator hπ = ∫ (g : G), ((toRepresentation ℂ G V π).symmetricPower 2).character g ∂TauCeti.haarProb G - ∫ (g : G), ((toRepresentation ℂ G V π).exteriorPower 2).character g ∂TauCeti.haarProb G

The Frobenius-Schur indicator is the signed difference of the two square-character integrals, ν₂(π) = ∫ χ_{Sym²π} - ∫ χ_{Λ²π}.

This is the Haar average of Representation.char_symmetricSquare_sub_char_exteriorSquare, which holds over every field, characteristic two included. Once the averaging projection identifies ∫ χ_ρ with the dimension of the invariants of ρ, the right-hand side becomes the signed count dim (Sym²V)ᴳ - dim (Λ²V)ᴳ of the finite-group statement.

theorem ContRepresentation.integral_character_sq {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : ∫ (g : G), (π.character hπ) g ^ 2 ∂TauCeti.haarProb G = ∫ (g : G), ((toRepresentation ℂ G V π).symmetricPower 2).character g ∂TauCeti.haarProb G + ∫ (g : G), ((toRepresentation ℂ G V π).exteriorPower 2).character g ∂TauCeti.haarProb G

The two square-character integrals add up to the integral of the squared character, ∫ χ_π² = ∫ χ_{Sym²π} + ∫ χ_{Λ²π}. Together with ContRepresentation.frobeniusSchurIndicator_eq_sub_integral this determines both.

theorem ContRepresentation.integral_character_symmetricPower_two {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : ∫ (g : G), ((toRepresentation ℂ G V π).symmetricPower 2).character g ∂TauCeti.haarProb G = (∫ (g : G), (π.character hπ) g ^ 2 ∂TauCeti.haarProb G + π.frobeniusSchurIndicator hπ) / 2

The symmetric-square character integrates to ½(∫ χ_π² + ν₂(π)).

theorem ContRepresentation.integral_character_exteriorPower_two {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) : ∫ (g : G), ((toRepresentation ℂ G V π).exteriorPower 2).character g ∂TauCeti.haarProb G = (∫ (g : G), (π.character hπ) g ^ 2 ∂TauCeti.haarProb G - π.frobeniusSchurIndicator hπ) / 2

The exterior-square character integrates to ½(∫ χ_π² - ν₂(π)).

@[simp]

theorem ContRepresentation.conj_frobeniusSchurIndicator {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) : (starRingEnd ℂ) (π.frobeniusSchurIndicator hπ) = π.frobeniusSchurIndicator hπ

The Frobenius-Schur indicator of a unitary representation is real.

Conjugating the character inverts its argument (ContRepresentation.character_apply_inv), and (g * g)⁻¹ = g⁻¹ * g⁻¹, so the conjugate indicator is the Haar average of g ↦ χ(g⁻¹ * g⁻¹). Haar measure on a compact group is inversion invariant, which returns that average to the original one.

@[simp]

theorem ContRepresentation.im_frobeniusSchurIndicator {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) : (π.frobeniusSchurIndicator hπ).im = 0

The Frobenius-Schur indicator of a unitary representation has vanishing imaginary part: it is a real number, the form in which the reality trichotomy ν₂ ∈ {1, 0, -1} is stated.

theorem ContRepresentation.norm_frobeniusSchurIndicator_le {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) : ‖π.frobeniusSchurIndicator hπ‖ ≤ ↑(Module.finrank ℂ V)

The Frobenius-Schur indicator of a unitary representation has modulus at most the dimension: every character value of a unitary representation does, and Haar measure is normalized.