Documentation

TauCeti.RepresentationTheory.Continuous.OrthogonalDecomposition

The orthogonal decomposition of a unitary representation into irreducibles #

A finite-dimensional unitary continuous representation of a group is an orthogonal internal direct sum of irreducible subrepresentations. This is the geometric — as opposed to lattice-theoretic — form of complete reducibility: not merely that every subrepresentation has a complement, but that the whole space is cut into finitely many mutually orthogonal irreducible blocks.

The proof is the classical descent. A nonzero subrepresentation of a finite-dimensional representation contains an atom of the lattice of subrepresentations (TauCeti.Representation.exists_isAtom_le), and an atom carries an irreducible representation (TauCeti.Representation.isIrreducible_toRepresentation_of_isAtom). Unitarity enters exactly once, to split off that atom orthogonally: the orthogonal complement of an invariant subspace is again invariant (TauCeti.ContRepresentation.IsUnitary.orthogonal_mem_invtSubmodule), so the remainder is a strictly smaller subrepresentation and the descent recurses on it.

No measure, no compactness, and no continuity of the representation are used: the argument runs on a ContRepresentation only because that is where TauCeti.ContRepresentation.IsUnitary lives, and the acting group may be arbitrary. For a compact group the unitarity hypothesis is what Weyl's unitarian trick in TauCeti.RepresentationTheory.Compact.Unitarizable is there to supply. That trick does not make π itself unitary — it conjugates it into a unitary representation — so the decomposition is also recorded in the form that consumes such a conjugation, with the blocks carried back to π along it.

Main results #

Implementation notes #

Invariant subspaces are carried as Subrepresentation π.toRepresentation rather than as bare submodules with an invariance side condition: the lattice operations, the atoms, and the toRepresentation needed to say "irreducible" are then all Mathlib's, and the translation to submodules is Subrepresentation.toSubmodule_le_toSubmodule and its relatives.

Orthogonality of the resulting family is stated as Mathlib's OrthogonalFamily, which unfolds to the pairwise vanishing of inner products between distinct blocks and is the form the orthogonal projection API consumes; DirectSum.IsInternal is then read off it through OrthogonalFamily.isInternal_iff.

References #

This is the target exists_orthogonal_irreducible_decomposition of Layer 2 of the compact-groups roadmap. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

source
theorem TauCeti.ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition {𝕜 : 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 π) :
∃ (n : ℕ) (U : Fin n → Subrepresentation (ContRepresentation.toRepresentation 𝕜 G V π)), (∀ (i : Fin n), (U i).toRepresentation.IsIrreducible) ∧ (OrthogonalFamily 𝕜 (fun (i : Fin n) => ↥(U i).toSubmodule) fun (i : Fin n) => (U i).toSubmodule.subtypeₗᵢ) ∧ (DirectSum.IsInternal fun (i : Fin n) => (U i).toSubmodule) ∧ Module.finrank 𝕜 V = ∑ i : Fin n, Module.finrank 𝕜 ↥(U i).toSubmodule

Complete reducibility, orthogonal internal form. A finite-dimensional unitary continuous representation of a group decomposes as an orthogonal internal direct sum of finitely many irreducible subrepresentations, and its dimension is the sum of theirs.

The four conclusions say, in order: each block is irreducible; distinct blocks are orthogonal; the blocks decompose the space as an internal direct sum; and the dimensions add up. Unitarity is essential: a general finite-dimensional representation need not decompose into irreducible subrepresentations at all, since an invariant subspace need not have an invariant complement. Unitarity supplies one, and supplies it orthogonally, which is what makes the descent go through and the resulting family orthogonal.

source
theorem TauCeti.ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition_of_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] {π : ContRepresentation 𝕜 G V} {e : V ≃L[𝕜] W} (he : IsUnitary (ContRepresentation.congr e π)) :
∃ (n : ℕ) (U : Fin n → Subrepresentation (ContRepresentation.toRepresentation 𝕜 G V π)), (∀ (i : Fin n), (U i).toRepresentation.IsIrreducible) ∧ (Pairwise fun (i j : Fin n) => ∀ v ∈ (U i).toSubmodule, ∀ w ∈ (U j).toSubmodule, inner 𝕜 (e v) (e w) = 0) ∧ (DirectSum.IsInternal fun (i : Fin n) => (U i).toSubmodule) ∧ Module.finrank 𝕜 V = ∑ i : Fin n, Module.finrank 𝕜 ↥(U i).toSubmodule

Complete reducibility for a unitarizable representation, orthogonal internal form. If a continuous linear equivalence e : V ≃L[𝕜] W conjugates π into a unitary representation congr e π, then π itself — not merely its unitary model — is an internal direct sum of finitely many irreducible subrepresentations, of dimensions adding up to dim V, whose images under e are pairwise orthogonal.

This is TauCeti.ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition carried back along the equivalence of continuous representations ContRepresentation.congrEquiv : π.Equiv (congr e π): each block U i of the unitary model pulls back to (U i).toSubmodule.map e.symm, which is π-invariant because e intertwines π with congr e π, and irreducibility, internality and the dimension count travel along the linear equivalence e.symm restricted to it.

Orthogonality is not stated inside V, which carries no inner product here: e is there precisely because π need not preserve one, and the form the blocks are orthogonal for is the invariant ⟪e ·, e ·⟫ pulled back from W. Only the unitary model needs an inner product, so V is asked for no more than a finite-dimensional normed space, as TauCeti.ContRepresentation.congr itself is. Nothing here uses finiteness or compactness of the acting group; a construction of an e is what such a hypothesis is for, Weyl's unitarian trick TauCeti.ContRepresentation.exists_isUnitary_congr being one.