MATHLIBANNEX / CANONICAL DECLARATION CARD

A character becomes a joint unit eigenvector

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity

theorem

Transfers a normalized GNS eigenvector to the given representation through a unitary with a specified direction.

Statement

Let be a nonzero complex -algebra, with no unit assumed and. Let be a complex Hilbert space and a -representation. Assume is nonzero irreducible and that every nonzero irreducible representation of of is unitarily equivalent to it. Let be its unital extension to . Write and . Let be a norm-closed unital -subalgebra and a character of distinct from . Then there is such that

Assumptions

No separability of is assumed, and is not assumed commutative. The existence of the specified character of is part of the input.

Conclusion

One unit vector is a joint eigenvector for every , with eigenvalues given by the very same prescribed character .

Proof route

Extend the character to a pure state; prove that its GNS restriction is nonzero; use the singleton comparison and the zero GNS norm of a centered element.

Proof steps

  1. Apply Pure-state extension of the prescribed character to this closed unital -subalgebra of the nonzero unital and its character . Obtain a pure state on with . Let be its GNS representation, where , and restrict it by .

  2. If for every , the GNS identity would give . Complex linearity and normalization would then give

    Restricting to contradicts . Thus is nonzero. Purity gives irreducibility of by Pure-state GNS irreducibility. Reducing subspaces for also reduce , so is irreducible.

  3. Apply the singleton condition to this nonzero irreducible to obtain a unitary equivalence. Extending it to the unitizations supplies a unitary with

    We use this chosen for the rest of the argument. It is unnecessary to identify it with a separately chosen earlier intertwiner.

  4. For , put . Multiplicativity and preservation of adjoints give and . Since the extension agrees with on , the GNS identity yields

    Therefore .

  5. Set . Unitarity gives . Substituting this same vector into the intertwining equation gives

    Cancel the injective to obtain the stated joint eigenvector equations.

Main citations

Lean source signature (exact)

theorem exists_unit_eigenvector_of_character_ne_infinity [Nontrivial A]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (D : StarSubalgebra ℂ (Unitization ℂ A))
    [IsClosed (D : Set (Unitization ℂ A))]
    (chi : WeakDual.characterSpace ℂ D)
    (hchi : chi ≠ infinityCharacterOn (A := A) D) :
    ∃ eta : H, ‖eta‖ = 1 ∧
      ∀ d : D, pi.unitization (d : Unitization ℂ A) eta = chi d • eta
In the source Mathematical meaning
[Nontrivial A] The algebra is nonzero: . This condition does not say whether a unit is assumed; that information comes from the surrounding -algebra structure.
(pi : NonUnitalCStarRepresentation A H) The specified -representation ; no unit-preservation equation is required.
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) The specified representation is nonzero irreducible, and every nonzero irreducible -representation of the same algebra is unitarily equivalent to it.
(D : StarSubalgebra ℂ (Unitization ℂ A)) A unital complex -subalgebra of ; commutativity is not a binder.
[IsClosed (D : Set (Unitization ℂ A))] is norm closed in the unitization.
(chi : WeakDual.characterSpace ℂ D) The prescribed nonzero complex character on .
(hchi : chi ≠ infinityCharacterOn (A := A) D) differs from restricted to .
∃ eta : H, ‖eta‖ = 1 ∧ One vector is chosen in the original , and its norm is one.
∀ d : D, pi.unitization (d : Unitization ℂ A) eta = chi d • eta For every element of , view it in and apply to this same ; the result is the scalar times .

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.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity

Accepted content SHA-256: 512142c7a49c0f027a090868bbe392fb4cf6b021093ea4b545f6e540f0cd8e97

Accepted source guide SHA-256: 9ff6087d3bf926864169aa171d528125120e603e13c7ce87e3cba1679e5eed4c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑