Scalar character of the minimal unitization

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.infinityCharacter

def

Defines the distinguished scalar-coordinate character of the minimal unitization.

Statement

Let A be a complex C*-algebra, not assumed unital, and form its minimal unitization Unitization ℂ A. The infinity character is the character induced by projection onto the scalar coordinate: it evaluates a unitization element at its ℂ component. It is a character of Unitization ℂ A, not of A itself.

Definition

infinityCharacter = CharacterSpace.equivAlgHom.symm (Unitization.fstHom ℂ A); infinityCharacter(c,a)=c.

Assumptions

Let A be a complex C*-algebra, not assumed unital, and form its minimal unitization Unitization ℂ A.

Conclusion

The infinity character is the character induced by projection onto the scalar coordinate: it evaluates a unitization element at its ℂ component. It is a character of Unitization ℂ A, not of A itself.

Main citations

Lean source signature (exact)

noncomputable def infinityCharacter :
    WeakDual.characterSpace ℂ (Unitization ℂ A)

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