Compact-operator conclusion for the unital singleton condition

MathlibAnnex.Analysis.CStarAlgebra.Representation.faithful_and_compactOperatorModel_of_singleton_amongNonUnital

theorem

Applies the nonunital compact-operator theorem to the same operator-valued map underlying a unital representation.

Statement

Let be a nonzero unital complex -algebra, let be a separable complex Hilbert space, and let be a unital -representation satisfying the singleton condition of R11. Then is injective and

Assumptions

The quantified irreducible representations in the singleton condition need not initially be packaged with a unit equation; R11 shows that nonzero irreducibility forces that equation. No separability assumption is made on .

Conclusion

The same map is a faithful compact-operator model. In particular, it gives a -isomorphism .

Proof route

View the same operator-valued function as a representation in the unit-free interface, apply the nonunital singleton theorem, and translate its conclusions back without changing any operator.

Proof steps

Let denote the same function , regarded in the representation interface that does not require a unit equation:
No operator is changed.
The hypothesis of R11 says exactly that represents the unique unitary-equivalence class of nonzero irreducible -representations. Apply Faithfulness and compact-operator model from a singleton representation to .
The output is injectivity of together with . Since for every , these are precisely injectivity of and .

Main citations

Lean source signature (exact)

theorem faithful_and_compactOperatorModel_of_singleton_amongNonUnital
    [Nontrivial A] [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) :
    Function.Injective pi ∧
      IsCompactOperatorModel pi.toNonUnitalStarAlgHom

In the source	Mathematical meaning
`[Nontrivial A]`	The algebra is nonzero: . Unit structure comes from the surrounding `[CStarAlgebra A]`, not from this condition.
`[TopologicalSpace.SeparableSpace H]`	The complex Hilbert space is separable.
`(pi : Representation A H)`	The specified unital -representation .
`(hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi)`	is nonzero irreducible and is unitarily equivalent to every nonzero irreducible -representation of , even when the input representation interface does not initially record unit preservation.
`Function.Injective pi`	Faithfulness of the original .
`pi.toNonUnitalStarAlgHom`	The same operator-valued map: for every ; only the unit equation is omitted from the data interface.
`IsCompactOperatorModel pi.toNonUnitalStarAlgHom`	The same map is injective and has image exactly .

Exact source and proof.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.faithful_and_compactOperatorModel_of_singleton_amongNonUnital

Accepted content SHA-256: 936294cbca18b24420eace805432491fc8ac9c46c1cf5712a079fa4514306de6

Accepted source guide SHA-256: c8849e0e5bea60662a4d8a779c25351288e6d23e378c8f28585039d81a738f07

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73