Eigenvector for a character distinct from the scalar character

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity

theorem

Produces a unit joint eigenvector whose eigenvalue character is the prescribed character distinct from the scalar character.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a complex Hilbert space; let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A; let D be a closed unital star subalgebra of Unitization ℂ A; and let χ be a character of D distinct from infinityCharacterOn D. No separability assumption on H is required. There is a unit vector η in H such that π.unitization(d)η=χ(d)η for every d in D.

Assumptions

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a complex Hilbert space; let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A; let D be a closed unital star subalgebra of Unitization ℂ A; and let χ be a character of D distinct from infinityCharacterOn D. No separability assumption on H is required.

Conclusion

There is a unit vector η in H such that π.unitization(d)η=χ(d)η for every d in D.

Proof route

The source extends χ to a pure state on the unitization, forms its GNS representation, and shows its restriction to A is nonzero because χ is distinct from the scalar character. The unique-class hypothesis gives unitary equivalence to π and transfers the normalized GNS cyclic vector to η, preserving the joint eigenvector equation.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

  Exact formal dependency; inspect the linked Card and exact source.

• MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension

  Exact formal dependency; inspect the linked Card and exact source.

• MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

  Exact formal dependency; inspect the linked Card and exact source.

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

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