Contravariant forms and Schur's lemma

Let G be a group with an involution g ↦ star g, such as GL n ℂ with the conjugate transpose. A sesquilinear pairing S of two representations ρ and σ of G is contravariant if S (ρ g x) y = S x (σ (star g) y) for all g, x, y. Such pairings are the analogue, for the involution star, of invariant pairings, and they are governed by Schur's lemma: a separating contravariant form B on ρ, for instance a nondegenerate one, turns a pairing S into an intertwining map T from σ to ρ with S x y = B x (T y) (Representation.exists_intertwiningMap_forall_apply_eq_apply). Hence:

• a contravariant pairing of two nonisomorphic irreducible representations vanishes (Representation.eq_zero_of_isEmpty_equiv);
• over an algebraically closed field a contravariant form on an irreducible representation is a scalar multiple of B (Representation.exists_forall_apply_eq_mul_apply), so a separating contravariant form is unique up to a scalar, if it exists.

Main results

• Representation.exists_intertwiningMap_forall_apply_eq_apply: a contravariant pairing is represented through a separating contravariant form by an intertwining map.
• Representation.eq_zero_of_isEmpty_equiv and Representation.exists_forall_apply_eq_mul_apply: the two cases of Schur's lemma.

theorem Representation.exists_intertwiningMap_forall_apply_eq_apply {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {G : Type u_4} [Monoid G] [StarMul G] (ρ : Representation 𝕜 G V) (σ : Representation 𝕜 G W) [FiniteDimensional 𝕜 V] {B : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hB : B.SeparatingRight) (hρ : ∀ (g : G) (x y : V), (B ((ρ g) x)) y = (B x) ((ρ (star g)) y)) {S : V →ₗ⋆[𝕜] W →ₗ[𝕜] 𝕜} (hS : ∀ (g : G) (x : V) (y : W), (S ((ρ g) x)) y = (S x) ((σ (star g)) y)) : ∃ (T : σ.IntertwiningMap ρ), ∀ (x : V) (y : W), (S x) y = (B x) (T y)

A contravariant pairing is an intertwining map. If B is a separating contravariant form on the finite-dimensional representation ρ, every contravariant pairing S of ρ with σ has the form S x y = B x (T y) for an intertwining map T from σ to ρ.

theorem Representation.eq_zero_of_isEmpty_equiv {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {G : Type u_4} [Monoid G] [StarMul G] (ρ : Representation 𝕜 G V) (σ : Representation 𝕜 G W) [FiniteDimensional 𝕜 V] [ρ.IsIrreducible] [σ.IsIrreducible] {B : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hB : B.SeparatingRight) (hρ : ∀ (g : G) (x y : V), (B ((ρ g) x)) y = (B x) ((ρ (star g)) y)) {S : V →ₗ⋆[𝕜] W →ₗ[𝕜] 𝕜} (hS : ∀ (g : G) (x : V) (y : W), (S ((ρ g) x)) y = (S x) ((σ (star g)) y)) (hne : IsEmpty (σ.Equiv ρ)) : S = 0

Schur's lemma for pairings of nonisomorphic representations. A contravariant pairing of two irreducible representations that are not isomorphic vanishes, provided the source carries a separating contravariant form.

theorem Representation.exists_forall_apply_eq_mul_apply {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {G : Type u_4} [Monoid G] [StarMul G] (ρ : Representation 𝕜 G V) [IsAlgClosed 𝕜] [FiniteDimensional 𝕜 V] [ρ.IsIrreducible] {B : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hB : B.SeparatingRight) (hρ : ∀ (g : G) (x y : V), (B ((ρ g) x)) y = (B x) ((ρ (star g)) y)) {S : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hS : ∀ (g : G) (x y : V), (S ((ρ g) x)) y = (S x) ((ρ (star g)) y)) : ∃ (c : 𝕜), ∀ (x y : V), (S x) y = c * (B x) y

Schur's lemma for contravariant forms. Over an algebraically closed field, a contravariant form on a finite-dimensional irreducible representation is a scalar multiple of any separating contravariant form.