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.

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.

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

Root-corner route explanation

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)
In the source Mathematical meaning
H; K is a complete complex Hilbert space; is a complex inner product space, with no completeness assumption.
ρ : Representation Limit H; hρ : ρ.IsIrreducible The given unital star representation of the CAR algebra has nonzero irreducible action.
n : ℕ; limitMatrixUnit n 0 0 The prescribed stage and its distinguished projection . Set and .
I; [Fintype I]; v : I → K A finite index set (possibly empty) and arbitrary input vectors ; independence and unit norm are not required.
∃ w : I → H There is one family of vectors satisfying both following requirements.
∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i For every , , equivalently .
∀ i j, inner ℂ (w i) (w j) = inner ℂ (v i) (v j) For every pair , the same family satisfies ; inner products are conjugate linear in the first entry. All entries of the Gram matrix agree.

Further source notes: No completeness assumption on K is hidden in the prose.

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.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram

Accepted content SHA-256: 5eb20e338e4667d68fe4fa0cc032f4f85d5495a2d970cb9f8159b36b668b3b76

Accepted source guide SHA-256: ae7a06a6d21656725bc075b158eb1e8d84c2297cf912d11bb2c50c795a57e622

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑