MATHLIBANNEX / CANONICAL DECLARATION CARD

Exact projection links for one approximately inner automorphism

MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner

theorem

A point-norm approximation followed by close-projection conjugacy gives exact support identities for an arbitrary projection family.

Statement

Let be a nonzero unital complex C*-algebra with its usual positive order, and let be a complex star automorphism. Suppose that for every finite and there is satisfying for all . For any set and family of self-adjoint projections in , there are elements such that and for every .

Assumptions

The same automorphism and its finite-set approximation property are fixed for the whole family. The index set is arbitrary. The projections need not be nonzero, orthogonal, or countably indexed, and no condition on their sum is imposed.

Conclusion

Each is a partial-isometry link with initial support and final support . The resulting links all use the one specified , although the auxiliary approximating and correcting unitaries may depend on .

The result gives algebraic support equations for the family. It asserts no convergence of a sum of links, no common correcting unitary, and no uniqueness of the chosen links. No pure-state or homogeneity hypothesis is needed once and its approximate innerness are supplied.

Proof route

For one projection , approximate within distance by . Close self-adjoint projections are exactly unitarily conjugate, so choose with . Then has the required supports. Apply this argument separately to each index and choose one link at each index.

Proof steps

  1. Approximate on the singleton with tolerance . Both and are self-adjoint projections and . The close-projection conjugacy theorem supplies with .

  2. For , the unitary identities and give . The other support is . Thus the direction of the two support equations is fixed.

  3. Use choice on the individual existence statements for . This produces a function with both equations at every index, including the vacuous case of an empty index set.

Main citations

Supporting route explanation

Lean source signature (exact)

theorem exists_shell_family_of_approximately_inner
    (A : Type u) {ι : Type v}
    [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A]
    (alpha : A ≃⋆ₐ[ℂ] A)
    (happrox : ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon →
      ∃ g : unitary A, ∀ a ∈ F,
        ‖alpha a - (g : A) * a * star (g : A)‖ < epsilon)
    (f : ι → A) (hf : ∀ i, IsStarProjection (f i)) :
    ∃ w : ι → A, ∀ i,
      star (w i) * w i = alpha (f i) ∧ w i * star (w i) = f i
In the source Mathematical meaning
A; [CStarAlgebra A]; [PartialOrder A]; [StarOrderedRing A]; [Nontrivial A] A nonzero unital complex C*-algebra with its usual positive order. This theorem is not restricted to CAR.
ι : Type v; alpha : A ≃⋆ₐ[ℂ] A An arbitrary index set and one fixed complex star automorphism .
happrox : ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon → ... For every finite and , there is one unitary satisfying for all . This assumption applies to the same for the whole family.
f : ι → A; hf : ∀ i, IsStarProjection (f i) The source family is the family in the text; each . The index set need not be countable and the projections need not be orthogonal or nonzero.
∃ w : ι → A, ∀ i There is one family of elements of with both following support equations for every .
star (w i) * w i = alpha (f i) The initial support is .
w i * star (w i) = f i The final support is . Both equations concern the same and the fixed ; these links need not be unitaries.

Further source notes: In the single-projection proof matchedLink g t (alpha f) is exactly . The first support is star w * w; it must not be interchanged with the second.

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.exists_shell_family_of_approximately_inner

Accepted content SHA-256: 7b5e7b90798dbd5ec276058cb2ce1adcd7e4c29e68375875478b7ba75774a9f8

Accepted source guide SHA-256: a230e2e80d7461106b2ebd36e31ab8a848be8cef9db391c301e39f6b46751bcf

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑