MATHLIBANNEX / CANONICAL DECLARATION CARD

An isolated character away from the scalar character

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_isolated_character_ne_infinity

theorem

Finds an isolated point in the open complement of the distinguished scalar character.

Statement

Let be a complex -algebra, with no unit assumed. On , write . Let be a norm-closed commutative unital -subalgebra of , and assume its character space is countable. Let be nonzero and have scalar coordinate zero. Then there is distinct from the scalar character such that is open in .

Assumptions

This theorem has no representation or singleton-representation hypothesis. Countability of the character space is an explicit input.

Conclusion

The same character is both different from the distinguished scalar character and isolated in the full character space.

Proof route

Use the nonzero element to show that the complement of the scalar character is nonempty, apply the countable Baire lemma in that open subspace, and transfer openness back.

Proof steps

  1. If every character vanished on , its Gelfand transform would be zero. Injectivity of the Gelfand transform would then give , a contradiction. Thus some satisfies . The scalar character has value zero at by the given scalar-coordinate condition, so .

  2. Set . The character space of the unital commutative -algebra is compact Hausdorff; hence the distinguished singleton is closed and is open. Step 1 shows . It is countable and as a subspace of , and it is Baire, since an open subspace of this locally compact Hausdorff space is locally compact Hausdorff.

  3. Apply An isolated point in a nonempty countable Baire space to this very subspace , using the four properties just verified. It supplies for which is open in . The inclusion of an open subspace is an open map, so the same singleton is open in . Membership in is precisely .

Main citations

Lean source signature (exact)

theorem exists_isolated_character_ne_infinity
    (D : StarSubalgebra ℂ (Unitization ℂ A))
    [IsClosed (D : Set (Unitization ℂ A))]
    [IsMulCommutative D]
    [Countable (WeakDual.characterSpace ℂ D)]
    (d : D) (hd : d ≠ 0)
    (hdfst : (d : Unitization ℂ A).fst = 0) :
    ∃ chi : WeakDual.characterSpace ℂ D,
      chi ≠ infinityCharacterOn (A := A) D ∧
        IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D))
In the source Mathematical meaning
(D : StarSubalgebra ℂ (Unitization ℂ A)) The unital complex -subalgebra of the unitization of the ordered possibly non-unital .
[IsClosed (D : Set (Unitization ℂ A))] is norm closed, hence a -algebra in its induced norm.
[IsMulCommutative D] Any two elements of commute.
[Countable (WeakDual.characterSpace ℂ D)] The full character space of is countable.
(d : D) (hd : d ≠ 0) A particular nonzero element of .
(hdfst : (d : Unitization ℂ A).fst = 0) When is viewed in , its scalar coordinate is zero; equivalently .
∃ chi : WeakDual.characterSpace ℂ D Choose one character of .
chi ≠ infinityCharacterOn (A := A) D That differs from the scalar character restricted to .
IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D)) The singleton of the same is open in the full character space, not merely in an unspecified subset.

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.exists_isolated_character_ne_infinity

Accepted content SHA-256: 765870c00eab1c0710f2c61041171ef3b65347d5aff7049c94991e04903047fc

Accepted source guide SHA-256: a6235f03b3079e4a690a58aa6cf570ff2747ec427946e82818a381d66ccd558d

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑