The Frobenius-Schur reality trichotomy for compact groups

For an irreducible unitary representation π of a compact group on a finite-dimensional complex inner product space, the Frobenius-Schur indicator takes only the three values

ν₂(π) = 1, ν₂(π) = 0, ν₂(π) = -1,

and which value occurs is read off the invariants of the symmetric and of the exterior square. This is the compact-group form of the finite-group TauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one.

Everything analytic is already done. ContRepresentation.frobeniusSchurIndicator_eq_sub_finrank_invariants, in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantTensors.lean, integrates the character identity and reads the indicator as the signed count of invariant tensors,

ν₂(π) = dim (Sym²V)ᴳ - dim (Λ²V)ᴳ.

What remained was the bound on the two counts, and that is pure linear algebra plus Schur's lemma: ContRepresentation.finrank_invariants_squares_le_one, in TauCeti/RepresentationTheory/Continuous/Square/Invariants.lean, says the two dimensions add up to at most 1, because the invariants of the tensor square of an irreducible are at most a line and the two squares meet in 0. A difference of two non-negative integers whose sum is at most 1 is 1, 0 or -1, and each value is pinned by which of the two squares carries the invariant.

The trichotomy is stated here for the indicator and the two invariant counts only. Its refinement into the invariant-form dictionary -- that ν₂ = 1 is the existence of a nonzero invariant symmetric bilinear form and ν₂ = -1 that of an invariant alternating one -- is TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantForm.lean, which reads the two invariant counts off invariant forms through TauCeti/RepresentationTheory/Continuous/Square/BilinearForm.lean; the finite-group version of that dictionary is TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Trichotomy.lean. What is still not established is the structure-map reformulation over ℝ, which reads the three values as the real, complex and quaternionic types.

Main statements

• ContRepresentation.frobeniusSchurIndicator_trichotomy: the indicator of an irreducible unitary representation of a compact group is 1, 0 or -1.
• ContRepresentation.frobeniusSchurIndicator_eq_one_iff_finrank_invariants_symmetricSquare, ContRepresentation.frobeniusSchurIndicator_eq_neg_one_iff_finrank_invariants_exteriorSquare and ContRepresentation.frobeniusSchurIndicator_eq_zero_iff_finrank_invariants_squares: which of the three values occurs, read off the invariants of the two squares.

References

This discharges the frobeniusSchurIndicator_trichotomy target of Layer 6b of the compact-groups roadmap, the step that its Suggested.lean pins on top of the indicator. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II.

theorem ContRepresentation.frobeniusSchurIndicator_trichotomy {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 : TauCeti.ContRepresentation.IsUnitary π) (hirr : (toRepresentation ℂ G V π).IsIrreducible) : π.frobeniusSchurIndicator hπ = 1 ∨ π.frobeniusSchurIndicator hπ = 0 ∨ π.frobeniusSchurIndicator hπ = -1

The Frobenius-Schur reality trichotomy for compact groups. The indicator of an irreducible unitary representation of a compact group on a finite-dimensional complex inner product space is 1, 0 or -1.

The indicator is the difference dim (Sym²V)ᴳ - dim (Λ²V)ᴳ (ContRepresentation.frobeniusSchurIndicator_eq_sub_finrank_invariants) and those two dimensions add up to at most 1 (ContRepresentation.finrank_invariants_squares_le_one), so the difference is one of the three values.

theorem ContRepresentation.frobeniusSchurIndicator_eq_one_iff_finrank_invariants_symmetricSquare {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 : TauCeti.ContRepresentation.IsUnitary π) (hirr : (toRepresentation ℂ G V π).IsIrreducible) : π.frobeniusSchurIndicator hπ = 1 ↔ Module.finrank ℂ ↥π.symmetricSquare.invariants = 1

The indicator is 1 exactly when the symmetric square carries a line of invariants.

theorem ContRepresentation.frobeniusSchurIndicator_eq_neg_one_iff_finrank_invariants_exteriorSquare {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 : TauCeti.ContRepresentation.IsUnitary π) (hirr : (toRepresentation ℂ G V π).IsIrreducible) : π.frobeniusSchurIndicator hπ = -1 ↔ Module.finrank ℂ ↥π.exteriorSquare.invariants = 1

The indicator is -1 exactly when the exterior square carries a line of invariants.

theorem ContRepresentation.frobeniusSchurIndicator_eq_zero_iff_finrank_invariants_squares {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 : TauCeti.ContRepresentation.IsUnitary π) (hirr : (toRepresentation ℂ G V π).IsIrreducible) : π.frobeniusSchurIndicator hπ = 0 ↔ Module.finrank ℂ ↥π.symmetricSquare.invariants = 0 ∧ Module.finrank ℂ ↥π.exteriorSquare.invariants = 0

The indicator is 0 exactly when neither square carries an invariant tensor.