The Frobenius-Schur trichotomy

TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariants computes the indicator ν₂(ρ) = |G|⁻¹ ∑_g χ(g²) as the signed count dim (Sym²V)ᴳ - dim (Λ²V)ᴳ of invariants in the two squares. This file identifies those two invariant counts with counts of bilinear forms on V, and reads the trichotomy off the identification.

The dictionary is elementary. A functional on Sym²V becomes a bilinear form on V by composing with the universal multilinear map, and the form it produces is symmetric because the symmetric square does not see the order of its two arguments; a functional on Λ²V becomes a form in the same way, and the form it produces is alternating because a repeated argument wedges to zero. Both assignments are injective. So the invariant functionals on the two squares inject into the invariant symmetric and the invariant alternating forms, which meet only in 0. Counting on the other side, the invariant forms are the intertwiners from ρ to its dual, and the character sum that counts those is the character sum that counts the invariants of the tensor square, read along g⁻¹ instead of g; so the two injections account for every invariant form, and

ν₂(ρ) = dim {invariant symmetric forms} - dim {invariant alternating forms}.

On an irreducible representation over an algebraically closed field the invariant forms are at most a line, and TauCeti.Representation.IsInvariantForm.isSymm_or_isAlt says a nonzero one is symmetric or alternating. The two counts are therefore 1, 0 or 0, 1 or 0, 0, which is the trichotomy: ν₂(ρ) is 1 when ρ carries a nonzero invariant symmetric form (the orthogonal case), -1 when it carries a nonzero invariant alternating form (the symplectic, or quaternionic, case), and 0 when it carries no nonzero invariant form at all (the complex case). The nonzero invariant form of the first two cases is automatically nondegenerate, by TauCeti.Representation.IsInvariantForm.nondegenerate.

Characteristic zero does three jobs, and nothing else: it moves the counting identities from equations in k to equations of natural numbers, it keeps a form from being symmetric and alternating at once, and it supplies Invertible (Nat.card G : k) in the statements that do not assume it. Averaging characters produces identities in k and nothing more, so the two counting identities are stated first in that form, needing only an invertible |G| (TauCeti.Representation.finrank_invariants_dual_cast and TauCeti.Representation.finrank_invariantForms_cast); in characteristic p they are identities of residues, and it is the injectivity of ℕ → k that turns them into equalities of dimensions.

Three ingredients come from earlier modules and are only applied here. The invariant forms themselves, the symmetric and the alternating ones among them, and their identification with the intertwiners into the dual are in TauCeti/RepresentationTheory/InvariantForm.lean; the dictionary turning a functional on either square into a form is TauCeti.BilinForm.ofSymmetricSquareDual and TauCeti.BilinForm.ofExteriorSquareDual, in TauCeti/LinearAlgebra/BilinearForm/Squares.lean; and the invariants of a dual representation, with their count, are in TauCeti/RepresentationTheory/Dual.lean. What this file adds is that the dictionary carries invariants to invariant forms, and the counting that follows.

Main results

• TauCeti.Representation.finrank_invariantForms: the invariant forms are as many as the invariants of the two squares together, as an identity in k whenever |G| is invertible (TauCeti.Representation.finrank_invariantForms_cast) and as natural numbers in characteristic zero.
• TauCeti.Representation.finrank_symmetricInvariantForms and TauCeti.Representation.finrank_alternatingInvariantForms: the two invariant form counts are the invariant counts of the two squares.
• TauCeti.Representation.map_ofSymmetricSquareDual_eq_symmetricInvariantForms and TauCeti.Representation.map_ofExteriorSquareDual_eq_alternatingInvariantForms: every invariant symmetric, respectively alternating, form comes from an invariant functional on the corresponding square.
• TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariantForms: the indicator is the signed count of invariant forms, ν₂(ρ) = dim {symmetric} - dim {alternating}.
• TauCeti.Representation.frobeniusSchurIndicator_eq_one_iff, TauCeti.Representation.frobeniusSchurIndicator_eq_neg_one_iff and TauCeti.Representation.frobeniusSchurIndicator_eq_zero_iff: the trichotomy, each value of the indicator characterized by the invariant forms, for an irreducible representation over an algebraically closed field of characteristic zero.
• TauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one: the indicator of such a representation takes only the values 1, 0 and -1.

Implementation notes

The two maps out of the dual squares are only ever used through their images: injectivity plus the dimension count is what forces them onto the symmetric and the alternating forms, in TauCeti.Representation.map_ofSymmetricSquareDual_eq_symmetricInvariantForms and TauCeti.Representation.map_ofExteriorSquareDual_eq_alternatingInvariantForms. Neither surjectivity is proved directly: on the symmetric side that would need a universal property of the symmetric square, which Mathlib does not have.

What connects the submodule of invariant forms to the character machinery is TauCeti.Representation.invariantFormsEquivIntertwiningMapDual: an equivalence with a space of intertwiners is the shape Mathlib's Representation.card_inv_mul_sum_char_mul_char_eq_finrank counts.

The dimension lemmas used below are stated for an abstract module and applied with that module supplied explicitly. The reason is mechanical: the AddCommMonoid structure on a space of bilinear forms is the one on linear maps, and asking the elaborator to solve for an AddCommGroup structure inducing it does not terminate quickly. The same is why the two range identities are stated with the image on the left: they come out of such a lemma in that orientation, and turning one round asks for exactly that comparison of structures.

References

• Character theory roadmap, Layer 7, “Invariant bilinear forms” and “The trichotomy”.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 4.

Invariant forms from invariant functionals on the two squares

theorem TauCeti.Representation.ofSymmetricSquareDual_mem_symmetricInvariantForms {k : Type} {G : Type v} {V : Type w} [CommRing k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {ψ : Module.Dual k (SymmetricPower k (Fin 2) V)} (hψ : ψ ∈ (ρ.symmetricPower 2).dual.invariants) : BilinForm.ofSymmetricSquareDual ψ ∈ symmetricInvariantForms ρ

An invariant functional on the symmetric square gives an invariant symmetric form.

theorem TauCeti.Representation.ofExteriorSquareDual_mem_alternatingInvariantForms {k : Type} {G : Type v} {V : Type w} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {ψ : Module.Dual k ↥(⋀[k]^2 V)} (hψ : ψ ∈ (ρ.exteriorPower 2).dual.invariants) : BilinForm.ofExteriorSquareDual ψ ∈ alternatingInvariantForms ρ

An invariant functional on the exterior square gives an invariant alternating form.

Counting the invariant forms

theorem TauCeti.Representation.finrank_invariantForms_eq_finrank_invariants_tprod_self_cast {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) : ↑(Module.finrank k ↥(invariantForms ρ)) = ↑(Module.finrank k ↥(ρ.tprod ρ).invariants)

The invariant forms are as many as the invariants of the tensor square, as an identity in k: the invariant forms are the intertwiners ρ → ρ.dual, and the character sum counting those is the character sum counting the invariants of ρ ⊗ ρ, read along g⁻¹ instead of g.

As with TauCeti.Representation.finrank_invariants_dual_cast, in characteristic p this is an identity of residues only.

theorem TauCeti.Representation.finrank_invariantForms_cast {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) : ↑(Module.finrank k ↥(invariantForms ρ)) = ↑(Module.finrank k ↥(ρ.symmetricPower 2).invariants) + ↑(Module.finrank k ↥(ρ.exteriorPower 2).invariants)

The invariant forms are as many as the invariants of the two squares together, as an identity in k: they are as many as the invariants of the tensor square, and TauCeti.Representation.finrank_invariants_tprod_self_cast splits that count in two.

As with TauCeti.Representation.finrank_invariants_dual_cast, in characteristic p this is an identity of residues only; see TauCeti.Representation.finrank_invariantForms for the characteristic-zero form.

theorem TauCeti.Representation.finrank_invariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Module.finrank k ↥(invariantForms ρ) = Module.finrank k ↥(ρ.symmetricPower 2).invariants + Module.finrank k ↥(ρ.exteriorPower 2).invariants

The invariant forms are as many as the invariants of the two squares together, as natural numbers. Characteristic zero is what lifts TauCeti.Representation.finrank_invariantForms_cast from an identity in k.

theorem TauCeti.Representation.finrank_symmetricInvariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Module.finrank k ↥(symmetricInvariantForms ρ) = Module.finrank k ↥(ρ.symmetricPower 2).invariants

The invariant symmetric forms are as many as the invariants of the symmetric square.

theorem TauCeti.Representation.finrank_alternatingInvariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Module.finrank k ↥(alternatingInvariantForms ρ) = Module.finrank k ↥(ρ.exteriorPower 2).invariants

The invariant alternating forms are as many as the invariants of the exterior square.

theorem TauCeti.Representation.map_ofSymmetricSquareDual_eq_symmetricInvariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Submodule.map BilinForm.ofSymmetricSquareDual (ρ.symmetricPower 2).dual.invariants = symmetricInvariantForms ρ

Every invariant symmetric form comes from an invariant functional on the symmetric square. The injection is onto: it lands in the invariant symmetric forms, and the two have the same dimension.

theorem TauCeti.Representation.map_ofExteriorSquareDual_eq_alternatingInvariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Submodule.map BilinForm.ofExteriorSquareDual (ρ.exteriorPower 2).dual.invariants = alternatingInvariantForms ρ

Every invariant alternating form comes from an invariant functional on the exterior square. The injection is onto: it lands in the invariant alternating forms, and the two have the same dimension.

theorem TauCeti.Representation.finrank_symmetricInvariantForms_add_finrank_alternatingInvariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Finite G] [CharZero k] (ρ : Representation k G V) : Module.finrank k ↥(symmetricInvariantForms ρ) + Module.finrank k ↥(alternatingInvariantForms ρ) = Module.finrank k ↥(invariantForms ρ)

The two invariant form counts add to the number of invariant forms.

The indicator as a signed count of invariant forms

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariantForms {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) : frobeniusSchurIndicator ρ = ↑(Module.finrank k ↥(symmetricInvariantForms ρ)) - ↑(Module.finrank k ↥(alternatingInvariantForms ρ))

The Frobenius-Schur indicator is the signed count of invariant bilinear forms, ν₂(ρ) = dim {invariant symmetric forms} - dim {invariant alternating forms}.

The trichotomy

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_zero_of_invariantForms_eq_bot {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (h : invariantForms ρ = ⊥) : frobeniusSchurIndicator ρ = 0

The complex case. A representation with no nonzero invariant form has Frobenius-Schur indicator 0.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_one_of_isSymm {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) (hsymm : B.IsSymm) : frobeniusSchurIndicator ρ = 1

The orthogonal case. An irreducible representation carrying a nonzero invariant symmetric form has Frobenius-Schur indicator 1. Such a form is automatically nondegenerate, by TauCeti.Representation.IsInvariantForm.nondegenerate.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_neg_one_of_isAlt {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) (halt : B.IsAlt) : frobeniusSchurIndicator ρ = -1

The symplectic case. An irreducible representation carrying a nonzero invariant alternating form has Frobenius-Schur indicator -1. Such a form is automatically nondegenerate, by TauCeti.Representation.IsInvariantForm.nondegenerate.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : frobeniusSchurIndicator ρ = 1 ∨ frobeniusSchurIndicator ρ = 0 ∨ frobeniusSchurIndicator ρ = -1

The Frobenius-Schur trichotomy. The indicator of an irreducible representation over an algebraically closed field of characteristic zero takes only the values 1, 0 and -1.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_one_iff {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : frobeniusSchurIndicator ρ = 1 ↔ ∃ (B : LinearMap.BilinForm k V), IsInvariantForm ρ B ∧ B.IsSymm ∧ B.Nondegenerate

The indicator is 1 exactly in the orthogonal case, that is, exactly when the representation carries a nondegenerate invariant symmetric form. Nondegeneracy is nonvanishing here, by TauCeti.Representation.IsInvariantForm.nondegenerate_iff_ne_zero.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_neg_one_iff {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : frobeniusSchurIndicator ρ = -1 ↔ ∃ (B : LinearMap.BilinForm k V), IsInvariantForm ρ B ∧ B.IsAlt ∧ B.Nondegenerate

The indicator is -1 exactly in the symplectic case, that is, exactly when the representation carries a nondegenerate invariant alternating form. Nondegeneracy is nonvanishing here, by TauCeti.Representation.IsInvariantForm.nondegenerate_iff_ne_zero.

theorem TauCeti.Representation.frobeniusSchurIndicator_eq_zero_iff {k : Type} {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : frobeniusSchurIndicator ρ = 0 ↔ invariantForms ρ = ⊥

The indicator is 0 exactly in the complex case, that is, exactly when the representation carries no nonzero invariant bilinear form at all.