MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

Main citations

Lean source signature (exact)

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

In the code, pi is , U is the family , and concreteTarget pi U is . The notation H →L[ℂ] H means a bounded complex-linear operator on ; →⋆ₐ[ℂ] denotes a unital complex-linear -homomorphism.

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 66b7b6935dd913a75006fffad6343b623e595b2a5ebbf7846d262b0d4849e125

Exposition revision: 1 · SHA-256: 8655c1a4a3f7e3a761fd34c830e74020310fd0c47245f74aaf8efcc1dec6ad4c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: e2dd36aeb72f45769069686cd03a443777c047101e021627f9ae23a900051b26

Back to top ↑