MATHLIBANNEX / CANONICAL DECLARATION CARD

A projection represented by a rank-one operator

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map

theorem

Obtains all projection, normalization, image and compactness conditions on the same witnesses.

Statement

Let be a nonzero complex -algebra, with no unit assumed. Let be a separable complex Hilbert space and a nonzero irreducible representation representing the unique unitary-equivalence class of nonzero irreducible comparisons. There are and such that where and the inner product is linear in its second argument. In particular, this same is compact.

Assumptions

Separability concerns . No prior faithfulness, simplicity, or unit in is assumed.

Conclusion

The chosen algebra projection has a rank-one orthogonal projection as its represented image, and that image is compact.

Proof route

Obtain a scalar-corner projection, use faithfulness to keep its image nonzero, apply the rank-one lemma, and substitute its image equation in compactness.

Proof steps

  1. Apply A nonzero scalar-corner projection to the given singleton and separable . It gives with for all . Apply Faithfulness on the original algebra to obtain injectivity of the same . Therefore would imply , so .

  2. Apply A scalar corner has a rank-one represented image to this same , its scalar-corner equations and the given irreducible . The reason its image has rank one is as follows. The operator is a nonzero orthogonal projection. Write on . If , then

    Choose a nonzero in the range of . Then , so . The unitized representation is irreducible, hence the orbit of is dense. Its image under lies in the closed one-dimensional subspace ; continuity therefore gives . The reverse inclusion follows from . For , the operator is thus the orthogonal projection onto , namely

  3. The operator is bounded and has one-dimensional range, so it is compact: the closure of the image of the unit ball is a closed bounded subset of the finite-dimensional space . Substituting gives compactness of the same . This does not assert that the entire subspace is a compact set. The same therefore satisfies all the stated clauses.

The proof obtains a scalar-corner projection, but minimality is not a separate field in the displayed conclusion.

Main citations

Lean source signature (exact)

theorem exists_nonzero_projection_rankOne_map [Nontrivial A]
    [PartialOrder A] [StarOrderedRing A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
      (∃ e : H, ‖e‖ = 1 ∧ pi p = InnerProductSpace.rankOne ℂ e e) ∧
      IsCompactOperator (pi p)
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.
[PartialOrder A] [StarOrderedRing A] These typeclasses provide the usual order on a -algebra, equivalently when is positive. They are used by the state and positivity arguments.
[TopologicalSpace.SeparableSpace H] The Hilbert space is separable.
(pi : NonUnitalCStarRepresentation A H) The representation of the possibly non-unital algebra.
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) Nonzero irreducibility of and the universal unitary-comparison condition.
∃ p : A, IsStarProjection p ∧ p ≠ 0 One algebra element is a nonzero self-adjoint idempotent.
(∃ e : H, ‖e‖ = 1 ∧ pi p = InnerProductSpace.rankOne ℂ e e) For that , one unit vector represents its image as the whole operator .
∧ IsCompactOperator (pi p) The image under that same of the closed unit ball of has compact closure. This is an explicit additional output clause.

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_nonzero_projection_rankOne_map

Accepted content SHA-256: 172b0e8121425ab5e0154fa310444b31a98dad301162cb5c81188c2d90c708bc

Accepted source guide SHA-256: c3299e18de7e9a62990a645190d257003c5168631bfe36e27abde83a8f874186

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑