The closed operator algebra generated by a representation and extra operators

MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget

def

Places a represented algebra and a chosen family of bounded operators in one concrete closed algebra.

Statement

Let be a unital complex algebra with an additive, multiplicatively reversing involution, and let be a complex Hilbert space. Write for its bounded complex-linear operators. Fix a unital complex-linear -homomorphism , that is, a representation satisfying . For any family in , form the norm-closed unital -subalgebra generated by and the . This is the concrete target .

Definition

Put . Let denote the smallest unital complex subalgebra of containing and closed under adjoints. Define , where the bar denotes operator-norm closure. Thus consists of operator-norm limits of finite complex linear combinations of finite products of members of and their adjoints, including the empty product . The adjoint in and the algebra operations restrict to .

Assumptions

The algebra is unital and associative over , with an additive involution satisfying and . The map preserves multiplication, the unit, complex scalars and this involution. The space is complete for its complex inner-product norm. The index set is arbitrary. No norm on , faithfulness of , or conjugate-linearity of the involution on is assumed.

Conclusion

The construction provides a closed unital star subalgebra containing the displayed operators. Write for , for the element represented by , and for inclusion. Then and . The inclusion is injective; if is injective, so is . These maps and their injectivity statements are the contextual facts cited below, not additional clauses of the defining declaration.

The closure is taken inside the given operator algebra. The construction does not assert simplicity or irreducibility, and it introduces no universal completion of . In particular, an arbitrary extra operator need not be unitary.

noncomputable def concreteTarget (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) : StarSubalgebra ℂ (H →L[ℂ] H) :=
  generated (Set.range pi ∪ Set.range U)

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

Earlier published Card and PDF