The Hom representation of two continuous representations

Given continuous representations π on V and ρ on W of a group G, the operators V →L[𝕜] W carry the conjugation action T ↦ ρ g ∘ T ∘ π g⁻¹. This file builds it as a ContRepresentation on the operator space, the continuous counterpart of Mathlib's Representation.linHom on V →ₗ[𝕜] W.

Two facts make the construction worth naming. Its invariants are exactly the continuous intertwiners: ρ g ∘ T ∘ π g⁻¹ = T for every g says precisely that T intertwines, so Mathlib's ContIntertwiningMap π ρ is the invariant subspace of this representation. And its character is χ_π(g⁻¹) · χ_ρ(g), because the operator space is the finite-dimensional V →ₗ[𝕜] W with the conjugation action, whose character Mathlib computes (Representation.char_linHom).

Together these turn a character integral into the dimension of a space of intertwiners: over a compact group, Haar-averaging this representation counts its invariants, which is what TauCeti/RepresentationTheory/Compact/Intertwiner/Dimension.lean does.

Restricting the two sides along the two projections of a product of groups gives the two-sided Hom representation ContRepresentation.biLinHom: for π on V over H and ρ on W over G it is the representation of G × H on V →L[𝕜] W on which (g, h) acts by T ↦ ρ g ∘ T ∘ π h⁻¹. It is the same construction, restricted along the two projections, so it needs nothing beyond what ContRepresentation.linHom needs. Taking H = G, W = V and ρ = π specializes it to the two-sided action of G × G on the operators of a single representation, which is how the Peter-Weyl block of a compact group is read.

The carrier is the operator space V →L[𝕜] W, not V →ₗ[𝕜] W: a ContRepresentation acts by continuous linear maps on a topological module, and the operator norm is what makes the operators one. In finite dimension the two carriers agree, and ContRepresentation.conj_linHom is that comparison, stated as the identity that transports Mathlib's algebraic conjugation action to this one along LinearMap.toContinuousLinearMap.

Main definitions

• ContRepresentation.linHom: the Hom representation T ↦ ρ g ∘ T ∘ π g⁻¹ on V →L[𝕜] W.
• ContRepresentation.biLinHom: its two-sided form, the representation of G × H on V →L[𝕜] W acting by (g, h) • T = ρ g ∘ T ∘ π h⁻¹.
• ContRepresentation.invariantsEquivContIntertwiningMap: its invariant subspace is the space of continuous intertwiners π →ⁱL ρ.

Main statements

• ContRepresentation.continuous_linHom and ContRepresentation.continuous_biLinHom: the Hom representation of two representations with continuous operator-valued action again has one, and likewise for the two-sided form.
• ContRepresentation.linHom_apply_eq_self_iff_isIntertwining: an operator is fixed by the conjugation action exactly when it intertwines, and ContRepresentation.mem_linHom_invariants_iff_isIntertwining: the same read on the invariant subspace.
• ContRepresentation.character_linHom: its character is χ_π(g⁻¹) · χ_ρ(g).

References

The algebraic originals are Mathlib's: Representation.linHom for the conjugation action, Representation.mem_linHom_invariants_iff_isIntertwining and Representation.invariantsEquivIntertwiningMap for the identification of its invariants with the intertwiners — of which ContRepresentation.linHom_apply_eq_self_iff_isIntertwining and ContRepresentation.invariantsEquivContIntertwiningMap are the continuous analogues, the first proved by transporting the algebraic one — and Representation.char_linHom for the character.

The Hom representation lets a character integral count intertwiners, the compact-group form of Mathlib's finite-group Representation.card_inv_mul_sum_char_mul_char_eq_finrank. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.linHom {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) : ContRepresentation 𝕜 G (V →L[𝕜] W)

The Hom representation of two continuous representations: G acts on the operators V →L[𝕜] W by conjugation, T ↦ ρ g ∘ T ∘ π g⁻¹.

This is the continuous counterpart of Mathlib's Representation.linHom, with the operator space in place of the space of all linear maps; the two agree in finite dimension by ContRepresentation.conj_linHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContRepresentation.linHom_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (g : G) (T : V →L[𝕜] W) : ((π.linHom ρ) g) T = ρ g ∘SL T ∘SL π g⁻¹

The action operators of the Hom representation are conjugation.

theorem ContRepresentation.linHom_apply_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (g : G) (T : V →L[𝕜] W) (v : V) : (((π.linHom ρ) g) T) v = (ρ g) (T ((π g⁻¹) v))

The Hom representation, evaluated at an operator and a vector.

theorem ContRepresentation.continuous_linHom {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) [TopologicalSpace G] [IsTopologicalGroup G] (hπ : Continuous ⇑π) (hρ : Continuous ⇑ρ) : Continuous ⇑(π.linHom ρ)

The Hom representation has a continuous operator-valued action. Conjugation is the composition of the two contractions of ContinuousLinearMap.compL by the separate actions, and inversion is continuous on a topological group.

noncomputable def ContRepresentation.biLinHom {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) : ContRepresentation 𝕜 (G × H) (V →L[𝕜] W)

The two-sided Hom representation of G × H on the operators V →L[𝕜] W, for π a representation of H on V and ρ one of G on W: (g, h) acts by T ↦ ρ g ∘ T ∘ π h⁻¹.

It is ContRepresentation.linHom of π against ρ, with the source copy restricted along the second projection of G × H and the target copy along the first; the two factors are ordered so that the first acts on the values of T and the second on its argument. Taking π = ρ is the two-sided action of G × G on the operators of a single representation.

Equations

• π.biLinHom ρ = (π.restrict (MonoidHom.snd G H)).linHom (ρ.restrict (MonoidHom.fst G H))

@[simp]

theorem ContRepresentation.biLinHom_apply {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) (p : G × H) (T : V →L[𝕜] W) : ((π.biLinHom ρ) p) T = ρ p.1 ∘SL T ∘SL π p.2⁻¹

The action operators of the two-sided Hom representation are two-sided conjugation.

theorem ContRepresentation.biLinHom_apply_apply {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) (p : G × H) (T : V →L[𝕜] W) (v : V) : (((π.biLinHom ρ) p) T) v = (ρ p.1) (T ((π p.2⁻¹) v))

The two-sided Hom representation, evaluated at an operator and a vector.

theorem ContRepresentation.biLinHom_apply_mk_one {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) (g : G) (T : V →L[𝕜] W) : ((π.biLinHom ρ) (g, 1)) T = ρ g ∘SL T

The first factor of the two-sided Hom representation acts on the values of an operator.

theorem ContRepresentation.biLinHom_apply_one_mk {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) (h : H) (T : V →L[𝕜] W) : ((π.biLinHom ρ) (1, h)) T = T ∘SL π h⁻¹

The second factor of the two-sided Hom representation acts on the argument of an operator.

theorem ContRepresentation.continuous_biLinHom {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} {W : Type u_5} [NontriviallyNormedField 𝕜] [Group G] [Group H] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 H V) (ρ : ContRepresentation 𝕜 G W) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H] [IsTopologicalGroup H] (hπ : Continuous ⇑π) (hρ : Continuous ⇑ρ) : Continuous ⇑(π.biLinHom ρ)

The two-sided Hom representation of two representations with continuous operator-valued action has one.

@[simp]

theorem ContRepresentation.linHom_apply_eq_self_iff_isIntertwining {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (T : V →L[𝕜] W) : (∀ (g : G), ρ g ∘SL T ∘SL π g⁻¹ = T) ↔ ∀ (g : G), T ∘SL π g = ρ g ∘SL T

An operator fixed by the conjugation action is exactly one that intertwines. This is Mathlib's Representation.mem_linHom_invariants_iff_isIntertwining for the algebraic Hom representation, read on the operator space: the invariance equation ρ g ∘ T ∘ π g⁻¹ = T and the intertwining equation T ∘ π g = ρ g ∘ T are equations of continuous linear maps exactly when their underlying linear maps agree.

The left-hand side is the simp-normal form of T ∈ (linHom π ρ).invariants, which ContRepresentation.mem_invariants and ContRepresentation.linHom_apply — both simp lemmas — reduce to it; stating the lemma this way, exactly as Mathlib states its algebraic original, is what makes it usable by simp. ContRepresentation.mem_linHom_invariants_iff_isIntertwining is the same fact phrased in terms of the invariant subspace.

theorem ContRepresentation.mem_linHom_invariants_iff_isIntertwining {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (T : V →L[𝕜] W) : T ∈ (π.linHom ρ).invariants ↔ ∀ (g : G), T ∘SL π g = ρ g ∘SL T

An operator is invariant in the Hom representation exactly when it intertwines. This is ContRepresentation.linHom_apply_eq_self_iff_isIntertwining phrased in terms of the invariant subspace, the form in which the invariants of the Hom representation are consumed.

This is not a simp lemma: ContRepresentation.mem_invariants is one, so the left-hand side is not in simp-normal form, and tagging it makes simpNF report "left-hand side simplifies".

theorem ContRepresentation.toContinuousLinearMap_mem_invariants_linHom {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (f : ContIntertwiningMap π ρ) : f.toContinuousLinearMap ∈ (π.linHom ρ).invariants

A continuous intertwiner is an invariant operator of the Hom representation.

noncomputable def ContRepresentation.invariantsEquivContIntertwiningMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) : ↥(π.linHom ρ).invariants ≃ₗ[𝕜] ContIntertwiningMap π ρ

The invariants of the Hom representation are the continuous intertwiners.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContRepresentation.invariantsEquivContIntertwiningMap_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (T : ↥(π.linHom ρ).invariants) : ((π.invariantsEquivContIntertwiningMap ρ) T).toContinuousLinearMap = ↑T

The equivalence with the intertwiners forgets the invariance proof.

@[simp]

theorem ContRepresentation.invariantsEquivContIntertwiningMap_symm_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (f : ContIntertwiningMap π ρ) : ↑((π.invariantsEquivContIntertwiningMap ρ).symm f) = f.toContinuousLinearMap

The inverse of the equivalence with the intertwiners forgets the intertwining proof.

theorem ContRepresentation.conj_linHom {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (g : G) : LinearMap.toContinuousLinearMap.conj (((toRepresentation 𝕜 G V π).linHom (toRepresentation 𝕜 G W ρ)) g) = ↑((π.linHom ρ) g)

The Hom representation is Mathlib's Representation.linHom, transported along LinearMap.toContinuousLinearMap. In finite dimension every linear map is continuous, and the resulting identification of V →ₗ[𝕜] W with V →L[𝕜] W conjugates the algebraic conjugation action into the one built here.

theorem ContRepresentation.character_linHom {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hπ : Continuous ⇑π) (hρ : Continuous ⇑ρ) (g : G) : ((π.linHom ρ).character ⋯) g = (π.character hπ) g⁻¹ * (ρ.character hρ) g

The character of the Hom representation is χ_π(g⁻¹) · χ_ρ(g). The trace is unchanged by transporting along LinearMap.toContinuousLinearMap, so this is Mathlib's Representation.char_linHom read on the operator space.