An irreducible operator algebra constructed from projection shells

MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel

theorem

Shell partial isometries with rank-one limiting defects can be completed to unitary links that join inequivalent irreducible fibers.

Statement

Let be a unital complex C*-algebra and a family of pairwise unitarily inequivalent irreducible unital representations on nonzero complete complex Hilbert spaces. Fix a root and unit vectors . On , let be coordinate inclusion, , and . For shell data satisfying the conditions below, there are unitaries such that and for all . The literal inclusion into of the norm-closed unital star algebra is irreducible.

Assumptions

For each , let and be decreasing subspaces of , with . All these subspaces and both intersections admit orthogonal projections. Write , , and , . The given bounded shell maps satisfy and . Their limiting defects are prescribed: and . Here , with the inner product linear in its second variable. No finite, countable or separable restriction is placed on the family. The rank-one conditions are input hypotheses of this generic theorem.

Conclusion

The same chosen family simultaneously has the unitary, vector-link and termwise-shell properties, and its concrete generated target acts irreducibly on . All closed reducing subspaces of that target action are therefore or .

Proof route

For each , sum the orthogonal shell maps strongly to an operator , then fill its one-dimensional defect by . To prove irreducibility, a bounded operator commuting with the target first has scalar diagonal blocks and zero off-diagonal blocks relative to the atomic source. Commuting with the links forces all those scalars to agree.

Proof steps

Apply the cited projection-shell rank-one completion theorem separately to each , with initial vector and final vector . Coordinate inclusion is isometric, so both vectors have norm one. The decreasing normalized flags, the two support equations and the two limiting projection identities are exactly its hypotheses. It supplies with strong convergence and the unitary completion . Choose these witnesses once for all .
The completion theorem also gives and . The rank-one correction vanishes on every initial difference shell because belongs to the limiting intersection. Thus the correction does not change any prescribed shell action.
Let commute with . Since and , it commutes with the atomic source and every link. The cited atomic-commutant theorem applies to the given irreducible, inequivalent fibers: each matrix block intertwines the corresponding actions; the Schur argument makes diagonal blocks scalar, while irreducibility and unitary inequivalence force off-diagonal blocks to vanish.
Write . Commuting with and evaluating at gives , hence since . Finite-support vectors are dense in the arbitrary-index Hilbert sum, so continuity yields on all of . Finally, the projection onto any closed reducing subspace commutes with ; being a scalar projection, it is or . This is the cited scalar-commutant irreducibility criterion.

Main citations

Lean source signature (exact)

theorem exists_irreducible_atomicShellModel
    (pi : ∀ i, Representation A (H i))
    (hirr : ∀ i, StarAlgHom.IsIrreducible (pi i))
    (hno : ∀ ⦃i j : I⦄, i ≠ j → ∀ e : H i ≃ₗᵢ[ℂ] H j,
      ¬ StarAlgHom.Intertwines (pi i) (pi j) (e : H i →L[ℂ] H j))
    (o : I) (xi : ∀ i, H i) (hxi : ∀ i, ‖xi i‖ = 1)
    (W : I → ℕ → HilbertSum H →L[ℂ] HilbertSum H)
    (U V : I → ℕ → Submodule ℂ (HilbertSum H))
    [∀ i n, (U i n).HasOrthogonalProjection]
    [∀ i n, (V i n).HasOrthogonalProjection]
    [∀ i, (⨅ n, U i n).HasOrthogonalProjection]
    [∀ i, (⨅ n, V i n).HasOrthogonalProjection]
    (hU : ∀ i, Antitone (U i)) (hV : ∀ i, Antitone (V i))
    (hU0 : ∀ i, U i 0 = ⊤) (hV0 : ∀ i, V i 0 = ⊤)
    (hInitial : ∀ i n, ((W i n)†).comp (W i n) =
      Submodule.projectionShell (U i) n)
    (hFinal : ∀ i n, (W i n).comp ((W i n)†) =
      Submodule.projectionShell (V i) n)
    (hUinf : ∀ i, (⨅ n, U i n).starProjection =
      InnerProductSpace.rankOne ℂ (coordinateEmbedding i (xi i))
        (coordinateEmbedding i (xi i)))
    (hVinf : ∀ i, (⨅ n, V i n).starProjection =
      InnerProductSpace.rankOne ℂ (coordinateEmbedding o (xi o))
        (coordinateEmbedding o (xi o))) :
    ∃ L : I → HilbertSum H →L[ℂ] HilbertSum H,
      (∀ i, L i ∈ unitary (HilbertSum H →L[ℂ] HilbertSum H)) ∧
      (∀ i, L i (coordinateEmbedding i (xi i)) =
        coordinateEmbedding o (xi o)) ∧
      (∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n) ∧
      Representation.IsIrreducible
        (ambientInclusion (atomicRepresentation pi) L)

Here pi i is , xi i is , and coordinateEmbedding i (xi i) is . U,V are the two flags; projectionShell (U i) n is . hUinf,hVinf supply the two rank-one defects. W i n is and L i is the completed unitary . For these continuous operators, postfix † is the adjoint written as superscript in the prose. ambientInclusion (atomicRepresentation pi) L is the inclusion of this same generated . The operators S and the commutant calculation occur in the linked proof, not as extra inputs in the signature.

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

Lean realization notes

This theorem does not assert , simplicity of , faithfulness of , or capture of every irreducible representation of . Its shell operators are not the cyclic-assembly map used in the later capture results. The star on operators is the Hilbert adjoint.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:2a90feae201a5ca31d5819e8ae349bc1c0ce60ba7b014b05aa3d7d8b1889f42e

Card revision: 1 · SHA-256: 2826da4e5a31e6b86b2bb133a8680ced9042a70adb452d4344a5f8f6b22f5791

Exposition revision: 1 · SHA-256: 95487527d395cd99f92f8c1a8240efcf23f237086442f81e625caaf494c1261e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 371e7613655011c5b77fd64394447cdbf4e82a9fddfcdcb90c58e792c19cd425