Full operator image in finite dimension

MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

theorem

Shows that an irreducible representation on a nonzero finite-dimensional Hilbert space has full operator image.

Statement

Let A be a unital complex C*-algebra, H a nonzero finite-dimensional complex Hilbert space, and π an irreducible unital representation of A on H. No singleton hypothesis or separability assumption on A is made. π is surjective onto all bounded complex-linear operators on H.

Assumptions

Let A be a unital complex C*-algebra, H a nonzero finite-dimensional complex Hilbert space, and π an irreducible unital representation of A on H. No singleton hypothesis or separability assumption on A is made.

Conclusion

π is surjective onto all bounded complex-linear operators on H.

Proof route

The source finds preimages separately for the self-adjoint real and imaginary parts of an arbitrary operator T using finite-dimensional irreducible interpolation. It combines those preimages as a+i b and invokes T=ℜT+iℑT.

Main citations

Lean source signature (exact)

theorem surjective_of_irreducible_of_finiteDimensional [Nontrivial H]
    [FiniteDimensional ℂ H]
    (pi : Representation A H) (hirr : pi.IsIrreducible) :
    Function.Surjective pi

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON