Documentation

TauCeti.RepresentationTheory.CharacterTable.FrobeniusSchur.Basic

The Frobenius-Schur indicator #

For a finite group G and a finite-dimensional representation ρ of G over a field k, the Frobenius-Schur indicator is the average of the character over squares, ν₂(ρ) = |G|⁻¹ ∑_g χ(g²).

The point of the indicator is what it counts. Mathlib's Representation.character averages to the dimension of the invariants (Representation.card_inv_mul_sum_char_eq_finrank), and Representation.char_symmetricSquare_sub_char_exteriorSquare says that the summand χ(g²) is the difference of the symmetric-square and exterior-square characters at g. Averaging that identity gives the main result of this file: the indicator is the signed count

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

of the invariants in the symmetric and exterior squares. Reading the companion identity Representation.char_tensorSquare the same way shows that those same two invariant dimensions sum to the dimension of the invariants of V ⊗ V.

Both identities are proved wherever |G| is invertible in k, with no hypothesis on characteristic two, because the two character identities they average hold over every field: the tensor square need not split for the two invariant counts to add up. The price is that a count of invariants only ever appears here through its image in k, so in characteristic p the additivity of the invariant dimensions is an identity of residues. Over a field of characteristic zero it upgrades to an equality of natural numbers, and there the indicator is an integer.

This is the module-level half of the roadmap's Layer 7 pair; the FDRep-level indicator and its agreement with this one are at the end of the file.

Main definitions #

Main results #

Implementation notes #

The definition asks only for a Fintype G: invertibility of |G| is a hypothesis of the theorems, not of the object. The two statements that do not mention the indicator ask only for Finite G, and build the Fintype they average over inside their proofs.

The FDRep-level indicator is the module-level one applied to V.ρ rather than a second copy of the average, so FDRep.frobeniusSchurIndicator_def unfolds that one definition and nothing else, and every theorem about the average transfers through it. Neither definition is @[expose]d, so the two _def lemmas are the only route to the two averages from another module; that is what they are for. It is also why both are proved by a parenthesised (rfl): a proof written syntactically as := rfl is implicitly tagged @[defeq], and validating that tag on an exported theorem asks that every definition it unfolds be exposed, which these two deliberately are not. The parentheses suppress the tag, which is what @[defeq]'s own documentation prescribes them for; a bare rfl does not compile here.

References #

source
noncomputable def TauCeti.Representation.frobeniusSchurIndicator {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
k

The Frobenius-Schur indicator of a representation of a finite group, ν₂(ρ) = |G|⁻¹ ∑_g χ(g²). It is the theorems below, not the average itself, that ask for V to be finite-dimensional and for |G| to be invertible in k.

Equations
Instances For
    source
    theorem TauCeti.Representation.frobeniusSchurIndicator_def {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
    frobeniusSchurIndicator ρ = (↑(Nat.card G))⁻¹ * ∑ g : G, ρ.character (g ^ 2)

    The defining equation of the indicator, ν₂(ρ) = |G|⁻¹ ∑_g χ(g²). The definition is not @[expose]d, so this is how it unfolds outside this file.

    source
    theorem TauCeti.Representation.frobeniusSchurIndicator_eq_of_equiv {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] {W : Type w'} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) :
    frobeniusSchurIndicator ρ = frobeniusSchurIndicator σ

    Equivalent representations have the same Frobenius-Schur indicator, since they have the same character.

    source
    @[simp]
    theorem TauCeti.Representation.frobeniusSchurIndicator_trivial {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] :
    frobeniusSchurIndicator (Representation.trivial k G V) = ↑(Module.finrank k V)

    The Frobenius-Schur indicator of a trivial representation is its dimension: every χ(g²) is dim V, and the average of a constant is that constant.

    source
    theorem TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariants {k : Type} {G : Type v} {V : Type w} [Field k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) :
    frobeniusSchurIndicator ρ = ↑(Module.finrank k ↥(ρ.symmetricPower 2).invariants) - ↑(Module.finrank k ↥(ρ.exteriorPower 2).invariants)

    The Frobenius-Schur indicator counts invariants in the two squares. Averaging Representation.char_symmetricSquare_sub_char_exteriorSquare over the group, ν₂(ρ) = dim (Sym²V)ᴳ - dim (Λ²V)ᴳ.

    This holds over every field in which |G| is invertible, characteristic two included, because the character identity it averages does; what fails in characteristic two is the splitting of the tensor square itself, not this count.

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

    The two invariant dimensions add to that of the tensor square, as an identity in k: averaging Representation.char_tensorSquare gives dim (V ⊗ V)ᴳ = dim (Sym²V)ᴳ + dim (Λ²V)ᴳ in k.

    As with TauCeti.Representation.frobeniusSchurIndicator_eq_sub_finrank_invariants, no hypothesis on characteristic two is needed: this is an equality of invariant dimensions, not a decomposition of the tensor square. In characteristic p it is an identity of residues only; see TauCeti.Representation.finrank_invariants_tprod_self for the characteristic-zero form.

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

    The two invariant dimensions add to that of the tensor square, as natural numbers: over a field of characteristic zero, dim (V ⊗ V)ᴳ = dim (Sym²V)ᴳ + dim (Λ²V)ᴳ.

    source
    theorem TauCeti.Representation.frobeniusSchurIndicator_eq_intCast {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 ↥(ρ.symmetricPower 2).invariants) - ↑(Module.finrank k ↥(ρ.exteriorPower 2).invariants))

    In characteristic zero the Frobenius-Schur indicator is an integer, namely the difference dim (Sym²V)ᴳ - dim (Λ²V)ᴳ of the two invariant counts. In characteristic zero |G| is automatically invertible, so no such hypothesis is needed.

    source
    noncomputable def FDRep.frobeniusSchurIndicator {k : Type} {G : Type v} [Field k] [Group G] [Fintype G] (V : FDRep k G) :
    k

    The Frobenius-Schur indicator of a finite-dimensional representation presented as an object of FDRep k G: the indicator |G|⁻¹ ∑_g χ(g²) of the underlying representation V.ρ.

    Equations
    Instances For
      source
      @[simp]
      theorem FDRep.frobeniusSchurIndicator_def {k : Type} {G : Type v} [Field k] [Group G] [Fintype G] (V : FDRep k G) :
      V.frobeniusSchurIndicator = TauCeti.Representation.frobeniusSchurIndicator V.ρ

      The two forms of the indicator agree: the FDRep-level indicator of V is the indicator of the underlying representation V.ρ. It is a simp lemma, so results proved on the module spine apply to the FDRep-level indicator automatically.