The character projections

The conjugate conj χ_π of the character of a continuous representation π of a compact group is a class function, so it acts on a finite-dimensional irreducible representation by a scalar (TauCeti.ContRepresentation.integratedOperator_eq_smul_id, from TauCeti/RepresentationTheory/Compact/Integrated.lean). Its Haar integral against another character χ_ρ is the L² inner product of the two characters, so the character orthogonality relations of TauCeti/RepresentationTheory/Compact/Character/Basic.lean evaluate that scalar. This file records the two resulting character projections, for π finite-dimensional irreducible and unitary:

• the kernel dim V_π · conj χ_π acts as the identity on V_π itself;
• conj χ_π acts as zero on a finite-dimensional ρ admitting no nonzero continuous intertwiner ρ → π.

These are the two blockwise identities from which the isotypic projectors are built. Their assembly on a reducible representation is carried out in TauCeti/RepresentationTheory/Compact/Character/IsotypicProjection.lean.

Main results

• ContRepresentation.integral_star_character_mul_character: pairing a character with the conjugate of another one is the L² inner product of the two characters.
• ContRepresentation.integratedOperator_star_character_self: conj χ_π acts on V_π by the scalar (dim V_π)⁻¹, so that, by ContRepresentation.finrank_smul_integratedOperator_star_character_self, the kernel dim V_π · conj χ_π acts as the identity on V_π.
• ContRepresentation.integratedOperator_star_character_eq_zero: for π unitary, conj χ_π acts as zero on a representation admitting no nonzero continuous intertwiner into π.

Implementation notes

The scalar in TauCeti.ContRepresentation.integratedOperator_eq_smul_id is (dim V)⁻¹ · ∫ f · χ_π, not ∫ f · conj χ_π: the integrand pairs the acting function with the character itself, and the conjugation appears only here, where the acting function is specialized to conj χ_π and ContRepresentation.integral_star_character_mul_character identifies the integral with Mathlib's sesquilinear L² inner product of the two characters.

References

These character-weighted averages give the operators used for isotypic projection and class-function completeness. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II.

theorem ContRepresentation.instCompleteSpaceProjectionSource {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

theorem ContRepresentation.instCompleteSpaceProjectionTarget {𝕜 : Type u_1} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] : CompleteSpace W

theorem ContRepresentation.integral_star_character_mul_character {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) : ∫ (g : G), (star (π.character hπ)) g * (ρ.character hρ) g ∂TauCeti.haarProb G = inner 𝕜 (π.characterLp hπ) (ρ.characterLp hρ)

Pairing a representation's character with the conjugate of another one's is the L² inner product of the two characters, in Mathlib's convention ⟪F, H⟫ = ∫ H · conj F. This is what turns the character orthogonality relations into statements about TauCeti.ContRepresentation.integratedOperator.

theorem ContRepresentation.integratedOperator_star_character_eq_zero {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : π.IsUnitary) (hdistinct : ∀ (φ : ContIntertwiningMap ρ π), φ.toContinuousLinearMap = 0) : TauCeti.ContRepresentation.integratedOperator ρ hρ (star (π.character hπ)) = 0

The character projection kills an inequivalent representation. If π is unitary and there is no nonzero continuous intertwiner ρ → π, the conjugate character of π acts as zero on ρ. Neither irreducibility of ρ nor algebraic closedness of 𝕜 is assumed.

Schur's lemma is not invoked for the intertwiner hypothesis; it is what supplies it for a pair of inequivalent irreducibles.

theorem ContRepresentation.integratedOperator_star_character_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) : TauCeti.ContRepresentation.integratedOperator π hπ (star (π.character hπ)) = (↑(Module.finrank 𝕜 V))⁻¹ • ContinuousLinearMap.id 𝕜 V

The conjugate character acts on its own representation by the inverse dimension. For a finite-dimensional irreducible unitary representation of dimension d, the integrated operator of conj χ_π on V_π is d⁻¹ • id.

The scalar is d⁻¹ rather than 1 exactly because the character has L² norm one: the projection kernel that acts as the identity is d · conj χ_π, which is ContRepresentation.finrank_smul_integratedOperator_star_character_self.

theorem ContRepresentation.finrank_smul_integratedOperator_star_character_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) : ↑(Module.finrank 𝕜 V) • TauCeti.ContRepresentation.integratedOperator π hπ (star (π.character hπ)) = ContinuousLinearMap.id 𝕜 V

The block projection, normalized. For a finite-dimensional irreducible unitary π, the kernel dim V_π · conj χ_π acts as the identity on V_π; together with ContRepresentation.integratedOperator_star_character_eq_zero, which makes it act as zero on a representation with no nonzero intertwiner into π, these are the two blockwise identities that characterize the isotypic projector attached to π. Assembling them into a projector on a reducible representation is done in TauCeti/RepresentationTheory/Compact/Character/IsotypicProjection.lean.