MATHLIBANNEX / CANONICAL DECLARATION CARD

The scalar character of the unitization

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.infinityCharacter

def

Names the character which reads the scalar coordinate and annihilates the embedded original algebra.

Statement

Let be a complex -algebra, with no unit assumed. Write its complex unitization as , with elements and inclusion . The scalar character is a character of .

Definition

Multiplication in the unitization is given by . Thus is a complex algebra homomorphism with , hence a nonzero character. The RHS below presents this very scalar-coordinate homomorphism as an element of the character space.

Assumptions

There is no nontriviality, order, separability, or representation-space hypothesis in this definition.

Conclusion

The resulting character satisfies , and consequently for every .

For a closed unital -subalgebra , the separate definition infinityCharacterOn D is its restriction . It is not a new character of .

Main citations

Lean source signature (exact)

The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.

/-- The scalar character of the minimal unitization. -/
noncomputable def infinityCharacter :
    WeakDual.characterSpace ℂ (Unitization ℂ A) :=
  WeakDual.CharacterSpace.equivAlgHom.symm (Unitization.fstHom (R := ℂ) (A := A))
In the source Mathematical meaning
Unitization ℂ A The complex unitization , not the original algebra alone.
WeakDual.characterSpace ℂ (Unitization ℂ A) The output belongs to the space of nonzero continuous complex characters of .
Unitization.fstHom (R := ℂ) (A := A) The algebra homomorphism .
WeakDual.CharacterSpace.equivAlgHom.symm Express that same homomorphism as a character; its value on each remains .

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.NonUnitalCStarRepresentation.infinityCharacter

Accepted content SHA-256: ba526c504b2c136abc501aaf70f88d96a67a20afa87f80f735d24b7398059540

Accepted source guide SHA-256: 35ef3ad0e85d28d6088d53affb966ecf16525d7f1ca2023518cf583713e01b0d

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑