Documentation

TauCeti.RepresentationTheory.Compact.FrobeniusSchur.InvariantTensors

The Frobenius-Schur indicator counts invariant tensors #

For a finite-dimensional continuous representation π of a compact group G, the Frobenius-Schur indicator ν₂(π) = ∫_G χ_π(g²) dμ of TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Basic.lean is the signed count of invariant tensors,

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

the compact-group form of the finite-group identity TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariants.

The two squares are realized inside the tensor square V ⊗[ℂ] V, as the two eigenspaces of the flip x ⊗ y ↦ y ⊗ x (TauCeti.symmetricTensors and TauCeti.antisymmetricTensors). That is not a matter of taste: Haar averaging counts the invariants of a continuous representation, so the carrier has to be a topological vector space, and the tensor square of a complex inner product space is one, whereas Sym[ℂ]^2 V and ⋀[ℂ]^2 V — a quotient and a subobject of a PiTensorProduct — carry no topology. In characteristic zero the eigenspaces are the symmetric and exterior squares, so nothing is lost.

With the squares realized that way the proof is short. The tensor square of π is ContRepresentation.tprod π π, the flip commutes with it, so each eigenspace is a subrepresentation, and their characters differ by χ_π(g²): this is ContRepresentation.character_symmetricSquare_sub_character_exteriorSquare, whose linear-algebra content is that composing f ⊗ f with the flip has trace tr (f ∘ f). Integrating that pointwise identity and reading each character integral as a dimension of invariants (ContRepresentation.integral_character_eq_finrank_invariants) is the theorem.

Neither the two squares nor their character identity needs any of the analysis, so neither is built here: the squares are defined and shown continuous, and their characters are compared, for a continuous representation of a monoid on an inner product space over RCLike 𝕜 in TauCeti/RepresentationTheory/Continuous/Square/Basic.lean and TauCeti/RepresentationTheory/Continuous/Square/Character.lean. Only the indicator statements below ask for a compact group and 𝕜 = ℂ.

Main statements #

Implementation notes #

The carrier of ContRepresentation.character is pinned by name at every use below, as character (𝕜 := ℂ) (V := symmetricTensors ℂ V) .... It has to be: the carrier is an implicit argument that the elaborator would have to read off the coercion ⇑(symmetricSquare π), and a submodule of V ⊗[ℂ] V receives its topology both as a subtype and through the norm its NormedAddCommGroup instance carries, so that unification stalls between the two instance paths. Pinning the carrier costs a few characters and makes every statement below elaborate on the first try.

References #

The indicator is defined in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Basic.lean, and the invariant counts use TauCeti/RepresentationTheory/Compact/Invariants.lean. The trichotomy ν₂ ∈ {1, 0, -1} is proved in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Trichotomy.lean. 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_sub_finrank_invariants {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 ⇑π) :
π.frobeniusSchurIndicator hπ = ↑(Module.finrank ℂ ↥π.symmetricSquare.invariants) - ↑(Module.finrank ℂ ↥π.exteriorSquare.invariants)

The Frobenius-Schur indicator is the signed count of invariant tensors, ν₂(π) = dim (Sym²V)ᴳ - dim (Λ²V)ᴳ.

Integrate ContRepresentation.character_symmetricSquare_sub_character_exteriorSquare and read each of the two character integrals as the dimension of the invariants of its representation (ContRepresentation.integral_character_eq_finrank_invariants). This is the compact-group form of the finite-group TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariants, with the Haar integral in place of the average over the group.

source
theorem ContRepresentation.frobeniusSchurIndicator_eq_intCast {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 ⇑π) :
π.frobeniusSchurIndicator hπ = ↑(↑(Module.finrank ℂ ↥π.symmetricSquare.invariants) - ↑(Module.finrank ℂ ↥π.exteriorSquare.invariants))

The Frobenius-Schur indicator of a compact group is an integer, being the difference of two dimensions. This is the first half of the reality trichotomy ν₂ ∈ {1, 0, -1}, and the compact-group form of the finite-group TauCeti.Representation.frobeniusSchurIndicator_eq_intCast; that the integer is one of 1, 0, -1 for an irreducible needs Schur's lemma and is not proved here.