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 .

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.

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.

Supporting route explanation

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)

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

Earlier published Card and PDF