Invariant complements of unitary continuous representations

For a unitary representation of a group the orthogonal complement of an invariant subspace is again invariant, so an invariant subspace admitting an orthogonal projection has an invariant complement. This is the averaging-free half of complete reducibility: it needs no measure, only that every action operator preserves the inner product.

Invariance of a submodule is Mathlib's Representation.invtSubmodule, the sublattice of submodules invariant under every action operator, and semisimplicity is Mathlib's Representation.IsSemisimpleRepresentation, the statement that the lattice of subrepresentations is complemented.

Main definitions

• ContRepresentation.IsUnitary.orthogonalSubrepresentation: the orthogonal complement of a subrepresentation of a unitary representation, as a subrepresentation.
• ContRepresentation.IsUnitary.starProjectionIntertwiner: the orthogonal projection onto an invariant subspace, as a continuous intertwining map.

Main results

• ContRepresentation.IsUnitary.orthogonal_mem_invtSubmodule: for a unitary representation of a group, the orthogonal complement of an invariant submodule is invariant. The element form is ContRepresentation.IsUnitary.apply_mem_orthogonal.
• ContRepresentation.IsUnitary.isCompl_orthogonalSubrepresentation: a subrepresentation admitting an orthogonal projection is complemented by its orthogonal complement.
• ContRepresentation.IsUnitary.sup_orthogonalSubrepresentation_inf: a subrepresentation together with its orthogonal complement inside a larger one recovers the larger one.
• ContRepresentation.IsUnitary.starProjection_apply_comm: the orthogonal projection onto an invariant subspace commutes with the action.
• ContRepresentation.IsUnitary.isSemisimpleRepresentation and ContRepresentation.IsUnitary.isSemisimpleModule_asModule: complete reducibility of a finite-dimensional unitary continuous representation, in the subrepresentation-lattice form and as semisimplicity of the group-algebra module.

Implementation notes

The hypothesis that G is a group is essential and is not a convenience: the unilateral shift is a unitary representation of the monoid ℕ on ℓ² for which the orthogonal complement of an invariant subspace need not be invariant. What the proof uses is that the action of g⁻¹ carries the invariant subspace back into itself.

Nothing here assumes V complete. Mathlib's ContinuousLinearMap.orthogonal_mem_invtSubmodule draws the same conclusion for a single operator T, from invariance under T.adjoint, but ContinuousLinearMap.adjoint is available only on a complete space, so that route would force [CompleteSpace V] on every statement below. Instead IsUnitary.inner_map_right moves the action across the inner product by inverting the group element, which needs no completeness. Mathlib keeps a completeness-free counterpart of the same result for symmetric operators, namely LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule.

Complementation of a single subrepresentation asks only for an orthogonal projection onto it. The semisimplicity statement, which asks it of every subrepresentation, is stated in finite dimensions, where every subspace is complete and hence has one. It is false for a general infinite-dimensional unitary representation, whose invariant subspaces decompose it as a Hilbert direct sum but not as an algebraic one.

References

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

The orthogonal complement of an invariant subspace

theorem ContRepresentation.IsUnitary.apply_mem_orthogonal {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} (hπ : π.IsUnitary) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) (g : G) {v : V} (hv : v ∈ Wᗮ) : (π g) v ∈ Wᗮ

For a unitary representation of a group, the action carries the orthogonal complement of an invariant subspace into itself.

theorem ContRepresentation.IsUnitary.orthogonal_mem_invtSubmodule {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} (hπ : π.IsUnitary) (hW : W ∈ (toRepresentation 𝕜 G V π).invtSubmodule) : Wᗮ ∈ (toRepresentation 𝕜 G V π).invtSubmodule

Invariant complements. For a unitary representation of a group, the orthogonal complement of an invariant submodule is again invariant.

def ContRepresentation.IsUnitary.orthogonalSubrepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (σ : Subrepresentation (toRepresentation 𝕜 G V π)) : Subrepresentation (toRepresentation 𝕜 G V π)

The orthogonal complement of a subrepresentation of a unitary representation, as a subrepresentation.

Equations

• hπ.orthogonalSubrepresentation σ = { toSubmodule := σ.toSubmoduleᗮ, apply_mem_toSubmodule := ⋯ }

@[simp]

theorem ContRepresentation.IsUnitary.toSubmodule_orthogonalSubrepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (σ : Subrepresentation (toRepresentation 𝕜 G V π)) : (hπ.orthogonalSubrepresentation σ).toSubmodule = σ.toSubmoduleᗮ

theorem ContRepresentation.IsUnitary.starProjection_apply_comm {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} [W.HasOrthogonalProjection] (hπ : π.IsUnitary) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) (g : G) (v : V) : W.starProjection ((π g) v) = (π g) (W.starProjection v)

The orthogonal projection onto an invariant subspace of a unitary representation commutes with the action.

noncomputable def ContRepresentation.IsUnitary.starProjectionIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} [W.HasOrthogonalProjection] (hπ : π.IsUnitary) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) : ContIntertwiningMap π π

The orthogonal projection onto an invariant subspace of a unitary representation, as a continuous intertwining map.

Equations

• hπ.starProjectionIntertwiner hW = { toContinuousLinearMap := W.starProjection, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.IsUnitary.toContinuousLinearMap_starProjectionIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} [W.HasOrthogonalProjection] (hπ : π.IsUnitary) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) : (hπ.starProjectionIntertwiner hW).toContinuousLinearMap = W.starProjection

@[simp]

theorem ContRepresentation.IsUnitary.starProjectionIntertwiner_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {W : Submodule 𝕜 V} [W.HasOrthogonalProjection] (hπ : π.IsUnitary) (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) (v : V) : (hπ.starProjectionIntertwiner hW) v = W.starProjection v

theorem ContRepresentation.IsUnitary.isCompl_orthogonalSubrepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (σ : Subrepresentation (toRepresentation 𝕜 G V π)) [σ.toSubmodule.HasOrthogonalProjection] : IsCompl σ (hπ.orthogonalSubrepresentation σ)

A subrepresentation of a unitary representation is complemented by its orthogonal complement, as soon as it admits an orthogonal projection.

theorem ContRepresentation.IsUnitary.sup_orthogonalSubrepresentation_inf {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) {σ τ : Subrepresentation (toRepresentation 𝕜 G V π)} (h : σ ≤ τ) [σ.toSubmodule.HasOrthogonalProjection] : σ ⊔ hπ.orthogonalSubrepresentation σ ⊓ τ = τ

A subrepresentation, together with its orthogonal complement taken inside a larger subrepresentation, recovers that larger subrepresentation. This is Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection read in the lattice of subrepresentations, which is legitimate because unitarity makes the orthogonal complement invariant.

Complete reducibility in finite dimensions

theorem ContRepresentation.IsUnitary.isSemisimpleRepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : (toRepresentation 𝕜 G V π).IsSemisimpleRepresentation

Complete reducibility. A finite-dimensional unitary continuous representation of a group is semisimple: every subrepresentation has a complement.

theorem ContRepresentation.IsUnitary.isSemisimpleModule_asModule {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : IsSemisimpleModule (MonoidAlgebra 𝕜 G) (toRepresentation 𝕜 G V π).asModule

Complete reducibility, algebraic form. The group-algebra module of a finite-dimensional unitary continuous representation of a group is semisimple.