The bilinear pairing of finite-group class functions

This file defines the normalized bilinear pairing on class functions of a finite group. When the coefficient field is algebraically closed and the group order is invertible, irreducible characters are orthonormal for this pairing.

The pairing is bilinear, rather than Hermitian: complex conjugation enters only after restricting to virtual characters.

Nondegeneracy is proved by pairing against the indicator function of a conjugacy class, TauCeti.ClassFunction.classIndicator. The value of that pairing, TauCeti.ClassFunction.characterPairing_classIndicator_inv, is of independent use: reading a class function off its pairings against the class indicators is what turns the expansion of a class function in the basis of irreducible characters into the second orthogonality relation.

References

• Character Theory roadmap, Layer 0.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 2.

noncomputable def TauCeti.ClassFunction.characterPairing {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] : LinearMap.BilinForm k ↥(ClassFunction k G)

The normalized bilinear pairing of class functions on a finite group.

Equations

• TauCeti.ClassFunction.characterPairing = LinearMap.mk₂ k (fun (f₁ f₂ : ↥(TauCeti.ClassFunction k G)) => (↑(Nat.card G))⁻¹ * ∑ g : G, ↑f₁ g * ↑f₂ g⁻¹) ⋯ ⋯ ⋯ ⋯

theorem TauCeti.ClassFunction.characterPairing_apply {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (f₁ f₂ : ↥(ClassFunction k G)) : (characterPairing f₁) f₂ = (↑(Nat.card G))⁻¹ * ∑ g : G, ↑f₁ g * ↑f₂ g⁻¹

The defining formula for the character pairing.

theorem TauCeti.ClassFunction.characterPairing_symm {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (f₁ f₂ : ↥(ClassFunction k G)) : (characterPairing f₁) f₂ = (characterPairing f₂) f₁

The character pairing is symmetric.

theorem TauCeti.ClassFunction.characterPairing_isSymm {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] : characterPairing.IsSymm

The bilinear form underlying characterPairing is symmetric.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_map {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {k' : Type u_1} [Field k'] (σ : k →+* k') (f₁ f₂ : ↥(ClassFunction k G)) : (characterPairing ((map σ) f₁)) ((map σ) f₂) = σ ((characterPairing f₁) f₂)

The character pairing commutes with a change of coefficient field: pairing the images of two class functions under a field homomorphism σ gives the image of their pairing.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_invMap_invMap {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (f₁ f₂ : ↥(ClassFunction k G)) : (characterPairing (invMap f₁)) (invMap f₂) = (characterPairing f₁) f₂

The character pairing is invariant under inverting the group element: the inversion twist TauCeti.ClassFunction.invMap is an isometry of the pairing.

theorem TauCeti.ClassFunction.characterPairing_classIndicator_inv {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (f : ↥(ClassFunction k G)) (x : G) : (characterPairing f) (classIndicator x⁻¹) = (↑(Nat.card G))⁻¹ * (↑(Nat.card ↑(ConjClasses.mk x).carrier) * ↑f x)

Pairing against a class indicator evaluates a class function. Pairing f with the indicator of the class of x⁻¹ returns the value of f at x, weighted by the size of the class of x and the normalization |G|⁻¹.

theorem TauCeti.ClassFunction.characterPairing_nondegenerate {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] : characterPairing.Nondegenerate

The character pairing is nondegenerate when the group order is invertible in the field.

theorem TauCeti.ClassFunction.characterPairing_ofCharacter {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (σ : Representation k G W) : (characterPairing (ofCharacter ρ)) (ofCharacter σ) = (↑(Nat.card G))⁻¹ * ∑ g : G, ρ.character g * σ.character g⁻¹

The pairing of two representation characters is Mathlib's normalized character sum.

theorem TauCeti.ClassFunction.characterPairing_ofFDRep {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (V W : FDRep k G) : (characterPairing (ofFDRep V)) (ofFDRep W) = (↑(Nat.card G))⁻¹ * ∑ g : G, V.character g * W.character g⁻¹

The pairing of two finite-dimensional representation characters is Mathlib's normalized character sum.

theorem TauCeti.ClassFunction.characterPairing_ofCharacter_eq_finrank {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) (σ : Representation k G W) : (characterPairing (ofCharacter ρ)) (ofCharacter σ) = ↑(Module.finrank k (σ.IntertwiningMap ρ))

The character pairing computes the dimension of an intertwiner space.

theorem TauCeti.ClassFunction.characterPairing_ofCharacter_sub_self {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) (σ : Representation k G W) [Subsingleton (σ.IntertwiningMap ρ)] : (characterPairing (ofCharacter ρ - ofCharacter σ)) (ofCharacter ρ - ofCharacter σ) = ↑(Module.finrank k (ρ.IntertwiningMap ρ)) + ↑(Module.finrank k (σ.IntertwiningMap σ))

When σ admits no nonzero intertwiner into ρ, the norm of χ_ρ - χ_σ is dim End(ρ) + dim End(σ): the cross terms are the dimensions of the intertwiner spaces between ρ and σ in the two directions, which agree by symmetry of the pairing.

theorem TauCeti.ClassFunction.characterPairing_ofCharacter_orthonormal {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] [Invertible ↑(Nat.card G)] [IsAlgClosed k] (ρ : Representation k G V) (σ : Representation k G W) [ρ.IsIrreducible] [σ.IsIrreducible] : (characterPairing (ofCharacter ρ)) (ofCharacter σ) = if Nonempty (σ.Equiv ρ) then 1 else 0

The character pairing of irreducible characters is Kronecker orthonormal.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_ofCharacter_self {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] [IsAlgClosed k] (ρ : Representation k G V) [ρ.IsIrreducible] : (characterPairing (ofCharacter ρ)) (ofCharacter ρ) = 1

An irreducible character pairs to 1 with itself.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_ofCharacter_eq_zero {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) (σ : Representation k G W) [ρ.IsIrreducible] [σ.IsIrreducible] (h : IsEmpty (σ.Equiv ρ)) : (characterPairing (ofCharacter ρ)) (ofCharacter σ) = 0

The characters of inequivalent irreducible representations pair to 0.

Algebraic closure is not needed here: by Schur's lemma the intertwiners between inequivalent irreducibles already form a subsingleton over any field.

theorem TauCeti.ClassFunction.characterPairing_ofFDRep_eq_finrank {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] (V W : FDRep k G) : (characterPairing (ofFDRep V)) (ofFDRep W) = ↑(Module.finrank k (W ⟶ V))

The character pairing computes the dimension of a morphism space in FDRep.

theorem TauCeti.ClassFunction.characterPairing_ofFDRep_orthonormal {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] : (characterPairing (ofFDRep V)) (ofFDRep W) = if Nonempty (V ≅ W) then 1 else 0

The character pairing of simple finite-dimensional representations is Kronecker orthonormal.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_ofFDRep_self {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] (V : FDRep k G) [CategoryTheory.Simple V] : (characterPairing (ofFDRep V)) (ofFDRep V) = 1

The character of a simple object of FDRep k G pairs to 1 with itself.

@[simp]

theorem TauCeti.ClassFunction.characterPairing_ofFDRep_eq_zero {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] (h : IsEmpty (V ≅ W)) : (characterPairing (ofFDRep V)) (ofFDRep W) = 0

The characters of non-isomorphic simple objects of FDRep k G pair to 0.

Algebraic closure is not needed here: by Schur's lemma the morphism space between non-isomorphic simple objects is already zero-dimensional over any field.