MATHLIBANNEX / CANONICAL DECLARATION CARD

Realizing a finite Gram matrix in a represented CAR corner

MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram

theorem

The infinite-dimensional root corner contains an isometric copy of any finite family of vectors.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. A representation is a unital complex star homomorphism into the bounded operators on a complex Hilbert space. Irreducibility means nonzero action and no proper nonzero closed reducing subspace. Fix an irreducible representation and a stage . Set and . Given any finite family in a complex inner product space , there are vectors with for every .

Assumptions

The space is a complex Hilbert space and has nonzero irreducible action. The space is only required to be a complex inner product space; completeness is not assumed. The finite index set may be empty, and the vectors need not be independent or normalized.

Conclusion

The entire Gram matrix is preserved inside one fixed represented root corner. Consequently all the norms and inner products of the family are retained. The corner and the stage are chosen before the input family is realized.

Proof route

The represented root projection has closed range, making a Hilbert space. Its range is infinite-dimensional, since otherwise its nonzero image would be compact. Embed the finite-dimensional span of the input family isometrically into .

Proof steps

  1. The finite matrix projection is self-adjoint and idempotent, and so is . Thus its range is closed and complete. The finite-corner identities underlying this choice are recorded in the short root-corner explanation linked below.

  2. If were finite-dimensional, would have finite rank and hence be compact. The no-compact-image theorem would imply , contradicting the injective stage inclusion. The precise result is not_finiteDimensional_range_rootCorner.

  3. The subspace is finite-dimensional. The finite-dimensional embedding theorem supplies a complex-linear isometry . Define , viewing each in . Preservation of inner products gives the required equalities.

Main citations

Lean source signature (exact)

theorem exists_rootCornerFamily_with_gram
    {H K : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    (ρ : Representation Limit H) (hρ : ρ.IsIrreducible)
    (n : ℕ) {I : Type*} [Fintype I] (v : I → K) :
    ∃ w : I → H,
      (∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) ∧
      ∀ i j, inner ℂ (w i) (w j) = inner ℂ (v i) (v j)

Here ρ is , limitMatrixUnit n 0 0 is , and is the range of its represented projection. The input v : I → K has arbitrary Gram matrix. The witness w : I → H is accompanied by ρ (...) (w i) = w i, which says that each vector lies in . No completeness assumption on K is hidden in the prose.

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

Lean realization notes

The finite-stage projection has rank one in , but is infinite-dimensional. The distinction is essential: the representation is of the completed algebra. The result gives a family in , not a preferred or unique choice of that family.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:3df5a5ce70663f3dc5301b1723671c1fa53f9bf40fc361fd6dee8f3b9199c2cb

Card revision: 1 · SHA-256: 29c4dbed8161f46b746ffc3fc519425c63d152562147a0982a71930f72a33f73

Exposition revision: 1 · SHA-256: e6478edabe7a2541aeebe042fff643bc896a50a591591056f659e5d8faac2957

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 8ac208272d8a53a8e22f64a2ff8cf3a2d41764d3a2bf9f6a1f9749be6fcb8c40

Back to top ↑