Structure maps and invariant bilinear forms, against a fixed invariant Hermitian form

An invariant bilinear form on an irreducible complex representation is strictly weaker than a structure map. Together with a positive definite invariant Hermitian form H, however, it produces one: this file builds a conjugate-linear equivariant map of V out of the two forms, and goes back again, so that against a fixed H one exists exactly when the other does.

Which structure map comes out is decided by the flip rule of the bilinear form. Writing B x y = ε * B y x -- with ε = 1 for a symmetric form and ε = -1 for an alternating one -- the map J produced squares to ε:

• a symmetric B gives a conjugate-linear involution, a Representation.IsRealStructure, whose real points are a real form;
• an alternating B gives a conjugate-linear J with J (J x) = -x, a Representation.IsQuaternionicStructure, whose fixed points are only 0.

Both cases are proved once here, for a real sign ε with ε * ε = 1, and specialized twice.

Comparing the two forms produces a conjugate-linear map J of V determined by H (J x) y = B x y. It exists because H, read as a map V → V*, is injective by definiteness and hence bijective -- as an ℝ-linear map between two spaces of the same finite real dimension -- so it can be inverted on the ℂ-linear map x ↦ B x. Invariance of both forms makes J commute with the action, so J ∘ J is a ℂ-linear self-intertwiner, and Schur's lemma over the algebraically closed ℂ forces J ∘ J = c • id. The flip rule of B and the Hermitian symmetry of H then evaluate c:

H (J x) (J x) = B x (J x) = ε * B (J x) x = ε * H (J (J x)) x = ε * conj c * H x x,

so ε * c is the ratio of two positive reals. Rescaling J by the inverse square root of that ratio -- a real scalar, so conjugate-linearity survives -- makes J ∘ J equal to ε: a real structure when ε = 1, a quaternionic one when ε = -1.

Only the two forms are needed, so nothing here asks for a finite group -- nor even for a group, since a definite invariant Hermitian form on a finite-dimensional space already makes each action map bijective, which is all the equivariance argument would use an inverse for. Producing the invariant Hermitian form is where finiteness enters, in TauCeti/RepresentationTheory/InvariantForm/Hermitian.lean, and the Frobenius-Schur criteria this feeds are in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Realizability.lean and TauCeti/RepresentationTheory/Compact/FrobeniusSchur/StructureMap.lean.

The converse passage, from a structure map K back to an invariant bilinear form, is the second half of the file, and it needs neither irreducibility nor finite dimensionality. The naive guess B x y = H (K x) y is bilinear, invariant and nondegenerate for free, but it obeys a flip rule only if H is compatible with K in the sense H (K x) (K y) = conj (H x y), which an arbitrary invariant H need not be. Replacing H by the balanced form LinearMap.balance H K x y = H x y + conj (H (K x) (K y)) of TauCeti/LinearAlgebra/SesquilinearForm/Balance.lean -- still invariant, Hermitian and positive definite, since K is bijective -- makes it compatible, and then B x y = H (K x) y flips by the sign that K ∘ K carries: symmetric for a real structure, alternating for a quaternionic one. Against a fixed H the two directions assemble into the existence criteria Representation.exists_isRealStructure_iff and Representation.exists_isQuaternionicStructure_iff, which are what turn the Frobenius-Schur values 1 and -1 into structure maps whenever a positive definite invariant Hermitian form is available -- by Haar averaging for a compact group as much as by summation for a finite one.

Main results

• Representation.exists_isRealStructure_of_isInvariantForm_of_isInvariantSesqForm: an irreducible representation carrying a nondegenerate invariant symmetric form and a nonnegative invariant Hermitian form that is definite off the origin has a real structure.
• Representation.exists_isQuaternionicStructure_of_isInvariantForm_of_isInvariantSesqForm: the same with an alternating form in place of a symmetric one produces a quaternionic structure.
• Representation.exists_isInvariantForm_isSymm_nondegenerate_of_isRealStructure: a real structure, together with a positive definite invariant Hermitian form, produces a nondegenerate invariant symmetric form.
• Representation.exists_isInvariantForm_isAlt_nondegenerate_of_isQuaternionicStructure: a quaternionic structure produces a nondegenerate invariant alternating form the same way.
• Representation.isInvariantSesqForm_balance: balancing an invariant sesquilinear form against an equivariant map leaves it invariant, which is what makes the balanced form of TauCeti/LinearAlgebra/SesquilinearForm/Balance.lean usable on a representation.
• Representation.exists_isRealStructure_iff and Representation.exists_isQuaternionicStructure_iff: against a positive definite invariant Hermitian form, an irreducible finite-dimensional representation has a real, respectively a quaternionic, structure exactly when it carries a nondegenerate invariant symmetric, respectively alternating, form.

Implementation notes

The two structure-map predicates are defined away from this file, so that stating one costs none of the machinery used to produce it: Representation.IsRealStructure in TauCeti/RepresentationTheory/RealForm.lean, beside the real-form theory that consumes it, and Representation.IsQuaternionicStructure in TauCeti/RepresentationTheory/QuaternionicStructure.lean, on its own -- nothing of that real-form theory attaches to it, since the fixed points of a J with J (J v) = -v are 0.

References

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II, §6.

Inverting a definite Hermitian form

The conjugate-linear map comparing the two forms

Equivariance and the Schur scalar

The structure maps

theorem Representation.exists_isRealStructure_of_isInvariantForm_of_isInvariantSesqForm {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [FiniteDimensional ℂ V] [ρ.IsIrreducible] {B : LinearMap.BilinForm ℂ V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hBinv : TauCeti.Representation.IsInvariantForm ρ B) (hBsymm : B.IsSymm) (hBnd : B.Nondegenerate) (hHinv : ρ.IsInvariantSesqForm H) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : ∃ (K : V →ₗ⋆[ℂ] V), ρ.IsRealStructure K

An invariant symmetric form and an invariant Hermitian form produce a real structure. This is the flip sign ε = 1 of the construction: the rescaled comparison map of the two forms is a conjugate-linear involution commuting with the action.

theorem Representation.exists_isQuaternionicStructure_of_isInvariantForm_of_isInvariantSesqForm {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [FiniteDimensional ℂ V] [ρ.IsIrreducible] {B : LinearMap.BilinForm ℂ V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hBinv : TauCeti.Representation.IsInvariantForm ρ B) (hBalt : B.IsAlt) (hBnd : B.Nondegenerate) (hHinv : ρ.IsInvariantSesqForm H) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : ∃ (J : V →ₗ⋆[ℂ] V), ρ.IsQuaternionicStructure J

An invariant alternating form and an invariant Hermitian form produce a quaternionic structure. This is the flip sign ε = -1 of the same construction, the only change being that the Schur scalar of the squared comparison map comes out negative, so that rescaling leaves a conjugate-linear J with J (J x) = -x rather than an involution.

An invariant bilinear form out of a structure map

theorem Representation.isInvariantSesqForm_balance {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} {K : V →ₗ⋆[ℂ] V} (hHinv : ρ.IsInvariantSesqForm H) (hK : ∀ (g : G) (v : V), K ((ρ g) v) = (ρ g) (K v)) : ρ.IsInvariantSesqForm (H.balance K)

The balanced form of an invariant sesquilinear form against an equivariant map is invariant. Both summands of LinearMap.balance H K are, the second because K commutes with the action. This is the only interaction between balancing and invariance that the passage from a structure map to an invariant bilinear form uses.

theorem Representation.exists_isInvariantForm_isSymm_nondegenerate_of_isRealStructure {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} {K : V →ₗ⋆[ℂ] V} (hK : ρ.IsRealStructure K) (hHinv : ρ.IsInvariantSesqForm H) (hHsymm : H.IsSymm) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm ρ B ∧ B.IsSymm ∧ B.Nondegenerate

A real structure produces a nondegenerate invariant symmetric form. This is the flip sign ε = 1 of the construction: the balanced form of H against the involution K is compatible with it, and B x y = H (K x) y is then symmetric.

theorem Representation.exists_isInvariantForm_isAlt_nondegenerate_of_isQuaternionicStructure {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} {J : V →ₗ⋆[ℂ] V} (hJ : ρ.IsQuaternionicStructure J) (hHinv : ρ.IsInvariantSesqForm H) (hHsymm : H.IsSymm) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm ρ B ∧ B.IsAlt ∧ B.Nondegenerate

A quaternionic structure produces a nondegenerate invariant alternating form. This is the flip sign ε = -1 of the same construction: the form built from J obeys B x y = -B y x, which over ℂ is alternation.

Each datum exists exactly when the other does

theorem Representation.exists_isRealStructure_iff {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [FiniteDimensional ℂ V] [ρ.IsIrreducible] {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hHinv : ρ.IsInvariantSesqForm H) (hHsymm : H.IsSymm) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : (∃ (K : V →ₗ⋆[ℂ] V), ρ.IsRealStructure K) ↔ ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm ρ B ∧ B.IsSymm ∧ B.Nondegenerate

Against a positive definite invariant Hermitian form, a real structure exists exactly when a nondegenerate invariant symmetric form does. Both directions are proved above; the Hermitian form is the fixed background datum, supplied by summation over a finite group or by Haar averaging over a compact one. This is an equivalence of the two existence statements, not of the two data: each direction produces some witness from a given one, and no inverse pair of constructions is claimed.

theorem Representation.exists_isQuaternionicStructure_iff {G : Type u_1} {V : Type u_2} [Monoid G] [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [FiniteDimensional ℂ V] [ρ.IsIrreducible] {H : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ} (hHinv : ρ.IsInvariantSesqForm H) (hHsymm : H.IsSymm) (hHnonneg : H.IsNonneg) (hdef : ∀ (x : V), x ≠ 0 → (H x) x ≠ 0) : (∃ (J : V →ₗ⋆[ℂ] V), ρ.IsQuaternionicStructure J) ↔ ∃ (B : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm ρ B ∧ B.IsAlt ∧ B.Nondegenerate

Against a positive definite invariant Hermitian form, a quaternionic structure exists exactly when a nondegenerate invariant alternating form does. This is the value -1 of the Frobenius-Schur trichotomy, Representation.exists_isRealStructure_iff being the value 1; the remaining value 0 is the case where no invariant bilinear form of either kind exists.