A character separates a closed ideal

MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem

theorem

Separates an element from a closed ideal of a commutative C*-algebra by a character vanishing on the ideal.

Statement

Let D be a commutative unital complex C*-algebra, J an ideal whose carrier is norm-closed, and d∈D with d∉J. There is a character χ of D that vanishes on every x∈J while χ(d)≠0. Properness follows from d∉J and is not separately assumed.

Assumptions

Let D be a commutative unital complex C*-algebra, J an ideal whose carrier is norm-closed, and d∈D with d∉J.

Conclusion

There is a character χ of D that vanishes on every x∈J while χ(d)≠0. Properness follows from d∉J and is not separately assumed.

Proof route

The source transports J through the Gelfand star transform to an ideal of continuous functions, uses isometry to preserve closedness and d∉J, then separates the transformed point by a character and pulls the annihilation/nonvanishing equations back.

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

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