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 .

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.

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

Root-corner route explanation

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)
In the source Mathematical meaning
H; [CompleteSpace H]; [Nontrivial H] A complete nonzero complex Hilbert space .
rho; hrho : StarAlgHom.IsIrreducible rho The unital star representation has no proper nonzero closed reducing subspace. Nonzero is explicit here.
n d : ℕ; rootCornerSubspace rho n Choose stage and family length . The corner space is , where .
v : Fin d → rootCornerSubspace rho n The finite family ; it need not span , and is allowed.
U : ... ≃ₗᵢ[ℂ] ...; hU : ∀ x, U (U x) = x A surjective complex-linear isometry with , for every .
∃ (h : selfAdjoint Limit) Choose one self-adjoint element with both support identities below.
heh : limitMatrixUnit n 0 0 * (h : Limit) = h The left support identity ; (h : Limit) reads the same self-adjoint element as an element of .
hhe : (h : Limit) * limitMatrixUnit n 0 0 = h The right support identity , for the same .
liftedCornerExponential n h heh hhe : Limit The unitary built from that . Here in is the imaginary unit.
∀ i, rho (...) (v i : H) = (U (v i) : H) For every family index , in . The coercions include the same corner vectors in . All prescribed actions use one and its unitary ; no action equality on the whole corner is required.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution

Accepted content SHA-256: 2173f9089f56ea2e070ce212de022348542c8805e9f48ab675b8eaf9a4976a2c

Accepted source guide SHA-256: faad1c125c6c755dafca4527c4664eec24a34e76a3c252a24397274417bca012

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑