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 .

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

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

Here the source family f i is in the prose, and alpha is the single fixed . hf supplies self-adjoint idempotence. 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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:d3588f1d2ec0d2fc4e2e95c0239994d0cc5b385bd89b3bf834ac79de13ae3fd5

Card revision: 1 · SHA-256: 3ff4e295253067a463fc1f1c82e2b18df098c20fd1732a982e33e0f635439d9e

Exposition revision: 1 · SHA-256: eef64486b674e07871709e723729417852b3bba75edc99a4828bc7e5b9a7a23b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 2c1e05303190fadc13fa812cc98cf91e9f06758a993fe193e786ed7b6d140d76

Back to top ↑