MATHLIBANNEX / CANONICAL DECLARATION CARD

A character separating a closed ideal

MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem

theorem

Finds one character which kills a closed ideal and detects a specified element outside it.

Statement

Let be a commutative unital complex -algebra, let be a norm-closed ideal, and let . There is a character such that A character here is a nonzero complex algebra homomorphism, hence unital and continuous.

Assumptions

Closedness is for the norm topology. Properness of and nontriviality of follow from ; they are not extra hypotheses.

Conclusion

The same character satisfies both annihilation of all of and nonvanishing at .

Proof route

Transport the ideal through the isometric Gelfand transform, find a point where the transformed element escapes its vanishing conditions, and evaluate there.

Proof steps

  1. Let be the character space of and its Gelfand -isomorphism, so . Put . Surjectivity and multiplicativity make an ideal. Since is an isometry and a homeomorphism, is closed. If , then for some , contradicting injectivity of and .

  2. Apply The closed-ideal description applied to this Gelfand image to the norm-closed ideal of continuous functions on the compact Hausdorff . It gives

    Since , there is with .

  3. For , the function belongs to , hence . At the distinguished element, . These are the two required conditions on the very same point of the character space.

Main citations

Lean source signature (exact)

theorem exists_character_annihilating_closedIdeal_of_not_mem
    {D : Type u} [CommCStarAlgebra D]
    (J : Ideal D) (hJclosed : IsClosed (J : Set D))
    {d : D} (hd : d ∉ J) :
    ∃ chi : WeakDual.characterSpace ℂ D,
      (∀ x : D, x ∈ J → chi x = 0) ∧ chi d ≠ 0
In the source Mathematical meaning
{D : Type u} [CommCStarAlgebra D] The commutative unital complex -algebra .
(J : Ideal D) (hJclosed : IsClosed (J : Set D)) The ideal and norm closedness of its set of elements.
{d : D} (hd : d ∉ J) A specified element outside that ideal.
∃ chi : WeakDual.characterSpace ℂ D Existence of one nonzero continuous complex character of .
(∀ x : D, x ∈ J → chi x = 0) This vanishes at every element belonging to .
∧ chi d ≠ 0 The same is nonzero at the chosen , in addition to all preceding vanishing equations.

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

Accepted content SHA-256: 3cff44bff4b25f76896443307bbf029be7560747e5fb8a7c407993ac6106da42

Accepted source guide SHA-256: d676b97b397cd148d14c3e7974c98391a12d187400cd925ecf11bfe22b105fb5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑