Isotypic projections for compact-group representations

Let sigma be a finite-dimensional continuous representation of a compact group. The continuous class function

dim(sigma) · conj(character sigma)

acts by integration on every finite-dimensional continuous representation rho. When sigma is irreducible and rho is unitary, the character-projection identities show that this action is the identity on every irreducible subrepresentation of rho isomorphic to sigma and zero on every other irreducible subrepresentation of rho. Complete reducibility then identifies its range with Mathlib's isotypicComponent of type sigma.

Main definitions

• ContRepresentation.isotypicKernel: the normalized conjugate-character kernel of sigma.
• ContRepresentation.isotypicProjector: its integrated action on rho, packaged as a continuous self-intertwiner of rho.

Main results

• ContRepresentation.isotypicKernel_eq_of_equiv, ContRepresentation.isotypicProjector_eq_of_equiv: kernel and projector depend on sigma only through its isomorphism type.
• ContRepresentation.isotypicProjector_apply_subtype_of_equiv: the projector is the identity on an irreducible subrepresentation of rho of the selected isomorphism type.
• ContRepresentation.isotypicProjector_apply_subtype_of_not_equiv: it vanishes on an irreducible subrepresentation of rho of every other isomorphism type.
• ContRepresentation.range_isotypicProjector: the range of the projector is precisely Mathlib's isotypicComponent.
• ContRepresentation.isotypicProjector_idempotent: the projector is idempotent.

Implementation notes

The selected irreducible sigma is an arbitrary continuous representation rather than a subrepresentation of rho: the kernel reads only its dimension and its character, and the vanishing statement concerns irreducibles that need not occur in rho at all. Isomorphism type is the only datum visible in the answer: the range is Mathlib's sum of the simple k[G]-submodules of rho.toRepresentation.asModule isomorphic to sigma.toRepresentation.asModule.

The carrier of sigma is only asked to be a finite-dimensional normed space; no inner product on it is required, since everything visible in the statements reads sigma through its dimension, its character and its isomorphism type. The results that see the whole of rho — the identity on a matching block, the range identification, the fixed-point characterization and idempotence — ask in addition that rho be unitary; the vanishing on a non-matching block does not.

References

The isotypic component is Mathlib's isotypicComponent. 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.

The kernel, the projector, and the matching blocks

theorem ContRepresentation.instCompleteSpaceIsotypicProjectionNormed {k : Type u_1} {V : Type u_3} [RCLike k] [NormedAddCommGroup V] [NormedSpace k V] [FiniteDimensional k V] : CompleteSpace V

noncomputable def ContRepresentation.isotypicKernel {k : Type u_1} {G : Type u_2} [RCLike k] [Group G] [TopologicalSpace G] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) : C(G, k)

The normalized conjugate-character kernel dim(sigma) · conj(character sigma) of a finite-dimensional continuous representation sigma. When sigma is irreducible, integrating this kernel on a finite-dimensional unitary representation cuts out its isotypic component of type sigma.

Equations

• sigma.isotypicKernel hsigma = ↑(Module.finrank k W) • star (sigma.character hsigma)

@[simp]

theorem ContRepresentation.isotypicKernel_apply {k : Type u_1} {G : Type u_2} [RCLike k] [Group G] [TopologicalSpace G] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (g : G) : (sigma.isotypicKernel hsigma) g = ↑(Module.finrank k W) * star ((sigma.character hsigma) g)

The value of the isotypic kernel.

theorem ContRepresentation.isotypicKernel_conj {k : Type u_1} {G : Type u_2} [RCLike k] [Group G] [TopologicalSpace G] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (g h : G) : (sigma.isotypicKernel hsigma) (h * g * h⁻¹) = (sigma.isotypicKernel hsigma) g

The isotypic kernel is constant on conjugacy classes.

theorem ContRepresentation.isotypicKernel_eq_of_equiv {k : Type u_1} {G : Type u_2} [RCLike k] [Group G] [TopologicalSpace G] {W : Type u_4} {W' : Type u_5} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] [NormedAddCommGroup W'] [NormedSpace k W'] [FiniteDimensional k W'] {sigma : ContRepresentation k G W} (hsigma : Continuous ⇑sigma) {tau : ContRepresentation k G W'} (htau : Continuous ⇑tau) (e : (toRepresentation k G W sigma).Equiv (toRepresentation k G W' tau)) : sigma.isotypicKernel hsigma = tau.isotypicKernel htau

Equivalent representations have the same normalized character kernel. The kernel sees sigma only through its isomorphism type.

noncomputable def ContRepresentation.isotypicProjector {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) : ContIntertwiningMap rho rho

The normalized character operator. This is the action on rho of dim(sigma) · conj(character sigma), packaged as a continuous self-intertwiner. When sigma is irreducible and the finite-dimensional representation rho is unitary, this operator is the isotypic projector onto the component of type sigma.

Equations

• rho.isotypicProjector hrho sigma hsigma = { toContinuousLinearMap := TauCeti.ContRepresentation.integratedOperator rho hrho (sigma.isotypicKernel hsigma), isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.toContinuousLinearMap_isotypicProjector {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) : (rho.isotypicProjector hrho sigma hsigma).toContinuousLinearMap = TauCeti.ContRepresentation.integratedOperator rho hrho (sigma.isotypicKernel hsigma)

The continuous linear map underlying the isotypic projector is the integrated action of the normalized conjugate-character kernel.

theorem ContRepresentation.isotypicProjector_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (v : V) : (rho.isotypicProjector hrho sigma hsigma) v = ∫ (g : G), (sigma.isotypicKernel hsigma) g • (rho g) v ∂TauCeti.haarProb G

The defining integral formula for the isotypic projector.

theorem ContRepresentation.isotypicProjector_eq_of_equiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} {W' : Type u_5} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] [NormedAddCommGroup W'] [NormedSpace k W'] [FiniteDimensional k W'] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) {sigma : ContRepresentation k G W} (hsigma : Continuous ⇑sigma) {tau : ContRepresentation k G W'} (htau : Continuous ⇑tau) (e : (toRepresentation k G W sigma).Equiv (toRepresentation k G W' tau)) : rho.isotypicProjector hrho sigma hsigma = rho.isotypicProjector hrho tau htau

Equivalent representations have the same isotypic projector. The projector sees sigma only through its isomorphism type.

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

theorem ContRepresentation.isotypicProjector_apply_subtype_of_equiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [IsAlgClosed k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (hunitary : rho.IsUnitary) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) {tau : Subrepresentation (toRepresentation k G V rho)} (htau : IsAtom tau) (e : Nonempty (↥tau.asSubmodule ≃ₗ[MonoidAlgebra k G] (toRepresentation k G W sigma).asModule)) (v : ↥tau.toSubmodule) : (rho.isotypicProjector hrho sigma hsigma) ↑v = ↑v

The isotypic projector is the identity on every equivalent irreducible block.

theorem ContRepresentation.isotypicProjector_apply_of_mem_isotypicComponent {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [IsAlgClosed k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (hunitary : rho.IsUnitary) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (hirr : (toRepresentation k G W sigma).IsIrreducible) (v : V) (hv : (toRepresentation k G V rho).asModuleEquiv.symm v ∈ isotypicComponent (MonoidAlgebra k G) (toRepresentation k G V rho).asModule (toRepresentation k G W sigma).asModule) : (rho.isotypicProjector hrho sigma hsigma) v = v

The isotypic projector fixes every vector in the selected isotypic component.

The non-matching blocks, the range and idempotence

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

theorem ContRepresentation.isotypicProjector_apply_subtype_of_not_equiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (hirr : (toRepresentation k G W sigma).IsIrreducible) {tau : Subrepresentation (toRepresentation k G V rho)} (htau : IsAtom tau) (hne : IsEmpty (↥tau.asSubmodule ≃ₗ[MonoidAlgebra k G] (toRepresentation k G W sigma).asModule)) (v : ↥tau.toSubmodule) : (rho.isotypicProjector hrho sigma hsigma) ↑v = 0

The isotypic projector vanishes on every inequivalent irreducible block.

@[simp]

theorem ContRepresentation.range_isotypicProjector {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [IsAlgClosed k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (hunitary : rho.IsUnitary) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (hirr : (toRepresentation k G W sigma).IsIrreducible) : (Representation.IntertwiningMap.range (toRepresentation k G V rho) (toRepresentation k G V rho) (rho.isotypicProjector hrho sigma hsigma).toIntertwiningMap).asSubmodule = isotypicComponent (MonoidAlgebra k G) (toRepresentation k G V rho).asModule (toRepresentation k G W sigma).asModule

The character projector cuts out the isotypic component. Its range is exactly Mathlib's sum of the simple k[G]-submodules isomorphic to the selected irreducible.

@[simp]

theorem ContRepresentation.mem_isotypicComponent_iff_isotypicProjector_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [IsAlgClosed k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (hunitary : rho.IsUnitary) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (hirr : (toRepresentation k G W sigma).IsIrreducible) (v : V) : v ∈ isotypicComponent (MonoidAlgebra k G) (toRepresentation k G V rho).asModule (toRepresentation k G W sigma).asModule ↔ (rho.isotypicProjector hrho sigma hsigma) v = v

A vector belongs to the selected isotypic component exactly when the character projector fixes it.

@[simp]

theorem ContRepresentation.isotypicProjector_idempotent {k : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike k] [IsAlgClosed k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace k V] [NormedSpace ℝ V] [SMulCommClass ℝ k V] [FiniteDimensional k V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace k W] [FiniteDimensional k W] (rho : ContRepresentation k G V) (hrho : Continuous ⇑rho) (hunitary : rho.IsUnitary) (sigma : ContRepresentation k G W) (hsigma : Continuous ⇑sigma) (hirr : (toRepresentation k G W sigma).IsIrreducible) : (rho.isotypicProjector hrho sigma hsigma).comp (rho.isotypicProjector hrho sigma hsigma) = rho.isotypicProjector hrho sigma hsigma

The character isotypic projector is idempotent.