MATHLIBANNEX / CANONICAL DECLARATION CARD

Full operator image in finite dimension

MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

theorem

Constructs a preimage of an arbitrary operator by separately lifting its self-adjoint real and imaginary parts.

Statement

Let be a unital complex -algebra and a nonzero finite-dimensional complex Hilbert space. If is an irreducible unital representation, then

Assumptions

No singleton condition, faithfulness or separability of is assumed. The finite-dimensionality and nontriviality hypotheses concern .

Conclusion

The image of is all bounded operators on .

Proof route

Interpolate each self-adjoint operator on the whole finite-dimensional space, then use the real-imaginary decomposition.

Proof steps

  1. For a self-adjoint bounded operator , apply Self-adjoint interpolation on a finite-dimensional subspace to the irreducible , the finite-dimensional subspace , and this . The theorem supplies a self-adjoint with for every (and a norm bound which is not needed here). Since , equality on all vectors gives . This is packaged in Preimages of self-adjoint operators on the whole finite-dimensional space.

  2. For an arbitrary , define

    Both operators are self-adjoint, so Step 1 gives with and .

  3. Use the same two preimages to set . Complex linearity gives

    This constructs the required preimage of each .

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
In the source Mathematical meaning
[Nontrivial H] The representation space is nonzero.
[FiniteDimensional ℂ H] The entire Hilbert space has a finite complex basis.
(pi : Representation A H) The unital -representation of the ordered unital -algebra .
(hirr : pi.IsIrreducible) This representation is nonzero and has no proper nonzero closed reducing subspace.
Function.Surjective pi For every bounded complex-linear operator , some algebra element satisfies as operators.

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

Accepted content SHA-256: cf06d584cd1fd1eb6baaf06b386ebd6e1a7b6f8dddcf1adb96c1b769b5529363

Accepted source guide SHA-256: edec39f02355afccce3e457cbbea41368524f4a5fb261ac23d30c7fbeabdc2b9

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑