MATHLIBANNEX / CANONICAL DECLARATION CARD

Lifting a corner involution to an ambient CAR unitary

MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution

theorem

A prescribed unitary involution on a represented root corner can be realized on finitely many vectors by one lifted corner exponential.

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. Let be a nonzero complex Hilbert space and an irreducible unital star representation. Fix a stage , put , and let . Suppose is a surjective complex-linear isometry with . For a finite family , there is , supported by on both sides, such that the unitary satisfies for every .

Assumptions

The Hilbert space is complete and nonzero; irreducibility here means that the representation has no proper nonzero closed reducing subspace. The integer may be zero. The selected vectors need not span . The involution is defined on the whole corner Hilbert space and is unitary there.

Conclusion

The same supported self-adjoint generator gives the ambient unitary and all the prescribed finite actions. Support means . The sum amplifies the corner unitary to a unitary of the unital algebra .

Proof route

The involution determines an orthogonal projection . Let be the zero extension of from to , where denotes the real circle constant. On the finite span of the selected vectors and their images under , acts as . Supported self-adjoint interpolation realizes this exponential by a corner element; matrix amplification preserves its action on root-corner vectors.

Proof steps

  1. Since is a unitary involution, is an orthogonal projection. Let be the zero extension of to . It is self-adjoint, has range in , and leaves the finite-dimensional space invariant. On , .

  2. The supported exponential interpolation result gives a self-adjoint whose corner exponential acts as on . Its proof first interpolates on with , then uses invariance of to compare the exponentials there.

  3. For , the matrix-unit amplification is unitary. On a root-corner vector its represented action reduces to that of . Hence . The route explanation below records the accompanying stage-central paths separately.

Main citations

Lean source signature (exact)

theorem exists_liftedCornerExponential_apply_eq_involution
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] [Nontrivial H]
    (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)
    (n d : ℕ) (v : Fin d → rootCornerSubspace rho n)
    (U : rootCornerSubspace rho n ≃ₗᵢ[ℂ] rootCornerSubspace rho n)
    (hU : ∀ x, U (U x) = x) :
    ∃ (h : selfAdjoint Limit)
      (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)
      (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h),
      ∀ i, rho (liftedCornerExponential n h heh hhe : Limit) (v i : H) =
        (U (v i) : H)

Here rootCornerSubspace rho n is , U is the corner isometry, and hU states . selfAdjoint Limit bundles ; heh and hhe express the two support identities. liftedCornerExponential is the matrix sum defining . In the proof, Complex.I is the imaginary unit; scalar pi and the representation rho are different objects.

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

Lean realization notes

Only the displayed finite family is required to have the prescribed action. The theorem does not identify the action on the whole corner with , and does not give a small-norm bound for . In this Hilbert-operator setting the source adjoint is the ordinary Hilbert adjoint ; the exact source notation is retained.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:68bfa7a5c5277bb3a0efdfd6f3fdbec6e079d8042e0ec7d2cab9a06db8b8fc32

Card revision: 1 · SHA-256: 32fb1332fb39aecd9f3eddad2225ee17f2bc95e81b086989d26eb6df3ff908f2

Exposition revision: 1 · SHA-256: 9bdd04f8f82e2692d889ad221fad61b384e764c97017b36fde237b1349e89982

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 48dea76422b7a6a8dd60db2c69ac0f88a55f71039cf015d35286e2f1f3871c01

Back to top ↑