Invariant sesquilinear forms on a representation

A sesquilinear form H : V →ₗ⋆[R] V →ₗ[R] R on the space of a representation ρ is invariant when every ρ g preserves it, H (ρ g x) (ρ g y) = H x y. This is the Hermitian companion of the bilinear TauCeti.Representation.IsInvariantForm, and the two together are what produce a real structure on a complex representation with Frobenius-Schur indicator 1.

The vocabulary and the construction that produces invariant forms use only the star-semiring algebra of the scalars, and are stated for a module over an arbitrary commutative star semiring: the invariant forms are a submodule of all sesquilinear forms, and summing an arbitrary form over the group makes it invariant, exactly as TauCeti/RepresentationTheory/InvariantForm/SumOfConjugates.lean does for a bilinear form.

Positivity is what asks for more, and the second half of the file is over ℂ. Here the sum does more work than it does over ℝ: there the sum of the coordinate dot products is merely nonzero, while over ℂ the sum of the coordinate Hermitian forms is still positive definite, because each summand is, and a sum of nonnegative complex numbers vanishes only when every summand does. So the construction gives an invariant inner product outright, not just a nonzero invariant form.

Positive semidefiniteness is Mathlib's LinearMap.IsPosSemidef for the complex order (activate it with open scoped ComplexOrder), which packages Hermitian symmetry conj (H x y) = H y x (LinearMap.IsSymm for the conjugation starRingEnd ℂ) together with 0 ≤ H x x. Definiteness is carried separately as H x x ≠ 0 off the origin, which is the form the Schur-lemma argument downstream consumes.

The positivity half is stated over ℂ rather than over an RCLike field. The order that LinearMap.IsPosSemidef needs is the one Complex.partialOrder supplies in the ComplexOrder scope, and RCLike supplies a second, lower-priority partial order in the same scope; stating the positivity results over RCLike would fix the wrong one of the two for the ℂ-only consumer, TauCeti/RepresentationTheory/InvariantForm/StructureMap.lean.

Main definitions

• Representation.IsInvariantSesqForm: a sesquilinear form invariant for a representation, with its unfolding Representation.isInvariantSesqForm_iff and the accessor Representation.IsInvariantSesqForm.apply.
• Representation.invariantSesqForms: the invariant sesquilinear forms, as a submodule of all sesquilinear forms on V.
• Representation.sumOfConjugatesSesqForm: the sum of a sesquilinear form over the conjugates of a representation of a finite monoid.

Main results

• Representation.isInvariantSesqForm_sumOfConjugatesSesqForm: that sum is invariant.
• Representation.isPosSemidef_sumOfConjugatesSesqForm: that sum is positive semidefinite if the form is.
• Representation.exists_isInvariantSesqForm_isPosSemidef_apply_self_ne_zero: a finite-dimensional complex representation of a finite group carries a positive definite invariant Hermitian form. This is the unitarian trick for a finite group, with the undivided sum in place of the average.
• Representation.IsInvariantSesqForm.surjective_of_apply_self_ne_zero: a definite invariant sesquilinear form on a finite-dimensional space makes every action map surjective, so a representation carrying one needs no group inverses.

References

• Character theory roadmap, Layer 7: the "compatible Hermitian form" that the realizability target frobeniusSchurIndicatorRep_eq_one_realizable is built from.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.

Invariant sesquilinear forms

def Representation.IsInvariantSesqForm {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : V →ₗ⋆[R] V →ₗ[R] R) : Prop

A sesquilinear form H is invariant for a representation ρ when every ρ g preserves it: H (ρ g x) (ρ g y) = H x y. This is the Hermitian companion of TauCeti.Representation.IsInvariantForm, stated pointwise because a sesquilinear form is out of reach of LinearMap.compl₁₂, which asks for a form linear in its first argument.

theorem Representation.isInvariantSesqForm_iff {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} : ρ.IsInvariantSesqForm H ↔ ∀ (g : G) (x y : V), (H ((ρ g) x)) ((ρ g) y) = (H x) y

A sesquilinear form is invariant for ρ exactly when it satisfies the pointwise equation H (ρ g x) (ρ g y) = H x y.

theorem Representation.IsInvariantSesqForm.apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} (hH : ρ.IsInvariantSesqForm H) (g : G) (x y : V) : (H ((ρ g) x)) ((ρ g) y) = (H x) y

An invariant sesquilinear form takes the same value on ρ g x and ρ g y as it does on x and y.

def Representation.invariantSesqForms {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) : Submodule R (V →ₗ⋆[R] V →ₗ[R] R)

The invariant sesquilinear forms of ρ, as a submodule of all sesquilinear forms on V.

@[simp]

theorem Representation.mem_invariantSesqForms {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} : H ∈ ρ.invariantSesqForms ↔ ρ.IsInvariantSesqForm H

Membership in Representation.invariantSesqForms is invariance.

@[simp]

theorem Representation.isInvariantSesqForm_zero {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} : ρ.IsInvariantSesqForm 0

The zero form is invariant.

theorem Representation.IsInvariantSesqForm.add {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H K : V →ₗ⋆[R] V →ₗ[R] R} (hH : ρ.IsInvariantSesqForm H) (hK : ρ.IsInvariantSesqForm K) : ρ.IsInvariantSesqForm (H + K)

A sum of invariant sesquilinear forms is invariant.

theorem Representation.IsInvariantSesqForm.smul {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} (c : R) (hH : ρ.IsInvariantSesqForm H) : ρ.IsInvariantSesqForm (c • H)

A scalar multiple of an invariant sesquilinear form is invariant.

def Representation.sumOfConjugatesSesqForm {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] [Fintype G] (ρ : Representation R G V) (H : V →ₗ⋆[R] V →ₗ[R] R) : V →ₗ⋆[R] V →ₗ[R] R

The sum of a sesquilinear form over the conjugates of a representation of a finite monoid, ∑ g, H (ρ g ·) (ρ g ·). No division by the order of the monoid is performed, exactly as in TauCeti.Representation.sumOfConjugatesForm for a bilinear form; when G is a group the plain sum is already invariant.

@[simp]

theorem Representation.sumOfConjugatesSesqForm_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] [Fintype G] (ρ : Representation R G V) (H : V →ₗ⋆[R] V →ₗ[R] R) (x y : V) : ((ρ.sumOfConjugatesSesqForm H) x) y = ∑ g : G, (H ((ρ g) x)) ((ρ g) y)

theorem Representation.isSymm_sumOfConjugatesSesqForm {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Monoid G] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} [Fintype G] (hH : H.IsSymm) : (ρ.sumOfConjugatesSesqForm H).IsSymm

The sum over the conjugates of a Hermitian form is Hermitian.

Surjectivity of the action

theorem Representation.IsInvariantSesqForm.surjective_of_apply_self_ne_zero {R : Type u_1} {G : Type u_2} {V : Type u_3} [Field R] [StarRing R] [Monoid G] [AddCommGroup V] [Module R V] [FiniteDimensional R V] {ρ : Representation R G V} {H : V →ₗ⋆[R] V →ₗ[R] R} (hH : ρ.IsInvariantSesqForm H) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) (g : G) : Function.Surjective ⇑(ρ g)

A definite invariant sesquilinear form makes the action surjective. Invariance carries the self-pairing of ρ g x back to that of x, so definiteness makes ρ g injective, and on a finite-dimensional space an injective endomorphism is surjective. A representation carrying such a form therefore needs no group inverses: an argument that would use ρ g⁻¹ to move a vector into the image of ρ g can use this instead, and so applies to a representation of a mere monoid.

Invariance of the conjugate sum

@[simp]

theorem Representation.isInvariantSesqForm_sumOfConjugatesSesqForm {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [StarRing R] [Group G] [Fintype G] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : V →ₗ⋆[R] V →ₗ[R] R) : ρ.IsInvariantSesqForm (ρ.sumOfConjugatesSesqForm H)

The sum of a sesquilinear form over the conjugates of a representation of a finite group is invariant: translating the summation index by h moves the sum for ρ h x and ρ h y back to the sum for x and y.

Positivity of the conjugate sum

theorem Representation.isNonneg_sumOfConjugatesSesqForm {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [AddCommMonoid V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hH : H.IsNonneg) : (ρ.sumOfConjugatesSesqForm H).IsNonneg

The sum over the conjugates of a nonnegative form is nonnegative.

theorem Representation.isPosSemidef_sumOfConjugatesSesqForm {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [AddCommMonoid V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hH : H.IsPosSemidef) : (ρ.sumOfConjugatesSesqForm H).IsPosSemidef

The sum over the conjugates of a positive semidefinite form is positive semidefinite.

theorem Representation.apply_self_eq_zero_of_sumOfConjugatesSesqForm_apply_self_eq_zero {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [AddCommMonoid V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hH : H.IsNonneg) {x : V} (hx : ((ρ.sumOfConjugatesSesqForm H) x) x = 0) : (H x) x = 0

A vector with vanishing self-pairing for the conjugate sum of a nonnegative form already has vanishing self-pairing for the form itself: the summand at g = 1 is one of the nonnegative summands of a vanishing sum.

The coordinate Hermitian form and the unitarian trick

theorem Representation.exists_isInvariantSesqForm_isPosSemidef_apply_self_ne_zero {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) [FiniteDimensional ℂ V] : ∃ (H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ), ρ.IsInvariantSesqForm H ∧ H.IsPosSemidef ∧ ∀ (x : V), x ≠ 0 → (H x) x ≠ 0

A finite-dimensional complex representation of a finite group carries a positive definite invariant Hermitian form. Take the coordinate Hermitian form of a basis -- the sesquilinear form of the identity matrix, ∑ i, conj (b.repr x i) * b.repr y i -- and sum it over the conjugates. The sum stays Hermitian and nonnegative, and it stays definite because a vanishing sum of nonnegative complex numbers has vanishing summands, in particular the one at g = 1.

This is the unitarian trick for a finite group, with the undivided sum in place of the average, so no invertibility of the group order is needed. Over ℝ the same recipe gives only a nonzero invariant form (TauCeti.Representation.exists_isInvariantForm_isSymm_ne_zero); it is the definiteness of the Hermitian form that makes this statement stronger.