Documentation

TauCeti.RepresentationTheory.Compact.FrobeniusSchur.InvariantForm

The Frobenius-Schur trichotomy of a compact group, read off invariant forms #

ContRepresentation.frobeniusSchurIndicator_trichotomy says that the indicator of an irreducible unitary representation of a compact group is 1, 0 or -1, and pins which value occurs by the invariants of the symmetric and of the exterior square. This file replaces those two invariant counts by invariant bilinear forms:

ν₂(π) = 1 iff π carries a nondegenerate invariant symmetric bilinear form, ν₂(π) = -1 iff it carries a nondegenerate invariant alternating one, ν₂(π) = 0 iff it carries no nonzero invariant bilinear form at all.

That is as far as this file goes: the classical reading of the three values as the real, complex and quaternionic types — that π is the complexification of a real representation, that it is not isomorphic to its conjugate, that it carries a quaternionic structure — is a further step, not proved here, since none of the statements below mentions a structure map or a real or quaternionic form.

The bridge is the inner-product dictionary of TauCeti/RepresentationTheory/Continuous/Square/BilinearForm.lean: a tensor t of V ⊗[ℂ] V becomes the form ⟪t, v ⊗ₜ w⟫, and that construction carries the symmetric tensors to the symmetric forms, the antisymmetric tensors to the alternating forms, and — because the representation is unitary — the invariant tensors to the invariant forms. So the two eigenspaces of the flip that the trichotomy counts are the invariant symmetric and the invariant alternating forms, and each of the three cases can be stated without mentioning the tensor square.

Two facts about an irreducible representation supply the rest, and both are consumed from TauCeti/RepresentationTheory/InvariantForm.lean: a nonzero invariant form on an irreducible representation is automatically nondegenerate (TauCeti.Representation.IsInvariantForm.nondegenerate), which is why the statements below ask for nondegeneracy rather than for nonvanishing; and over an algebraically closed field away from characteristic two it carries a nonzero invariant symmetric form, a nonzero invariant alternating one, or no nonzero invariant form at all (TauCeti.Representation.exists_isSymm_or_exists_isAlt_or_invariantForms_eq_bot), which is what makes the vanishing case ν₂ = 0 say that there is no invariant form at all.

This is the compact-group mirror of the finite-group TauCeti.Representation.frobeniusSchurIndicator_eq_one_iff and its companions in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Trichotomy.lean, and the statements are deliberately given the same shape: invariance is the named predicate TauCeti.Representation.IsInvariantForm, which unfolds to B (π g v) (π g w) = B v w, and the B ≠ 0 clause is left out because nondegeneracy already implies it (TauCeti.Representation.IsInvariantForm.nondegenerate_iff_ne_zero).

Main statements #

Implementation notes #

The first two theorems are one argument read twice, so both go through the private ContRepresentation.finrank_eq_one_iff_exists_nondegenerate: a count of invariants that is at most 1 is 1 exactly when a nonzero invariant form of the relevant kind exists, and on an irreducible representation "nonzero" and "nondegenerate" agree. The third then needs no count of its own: the trichotomy leaves only the values 1 and -1 to exclude, and those are exactly what the first two theorems name.

References #

This discharges the frobeniusSchurIndicator_eq_one_iff and frobeniusSchurIndicator_eq_neg_one_iff targets of Layer 6b of the compact-groups roadmap, the invariant-form dictionary its Suggested.lean pins on top of the trichotomy. 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.

source
theorem ContRepresentation.frobeniusSchurIndicator_eq_one_iff {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 ↔ ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm (toRepresentation ℂ G V π) B ∧ B.IsSymm ∧ B.Nondegenerate

The indicator is 1 exactly when there is an invariant symmetric form: an irreducible unitary representation of a compact group has Frobenius-Schur indicator 1 exactly when it carries a nondegenerate invariant symmetric bilinear form.

source
theorem ContRepresentation.frobeniusSchurIndicator_eq_neg_one_iff {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 ↔ ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm (toRepresentation ℂ G V π) B ∧ B.IsAlt ∧ B.Nondegenerate

The indicator is -1 exactly when there is an invariant alternating form: an irreducible unitary representation of a compact group has Frobenius-Schur indicator -1 exactly when it carries a nondegenerate invariant alternating bilinear form.

source
theorem ContRepresentation.frobeniusSchurIndicator_eq_zero_iff {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 ↔ TauCeti.Representation.invariantForms (toRepresentation ℂ G V π) = ⊥

The indicator is 0 exactly when there is no invariant form: an irreducible unitary representation of a compact group has Frobenius-Schur indicator 0 exactly when it carries no nonzero invariant bilinear form at all.

Over ℂ an irreducible representation carries a nonzero invariant symmetric form, a nonzero invariant alternating one, or no nonzero invariant form at all (TauCeti.Representation.exists_isSymm_or_exists_isAlt_or_invariantForms_eq_bot), so the two preceding theorems account for every invariant form, and the trichotomy leaves nothing else for the indicator to be.