A maximal abelian subalgebra containing a self-adjoint element

MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

theorem

Starts with the algebra generated by the given element and extends it by inclusion-maximality.

Statement

Let be a unital complex -algebra and let satisfy . There is a unital -subalgebra which contains and is maximal among commutative unital -subalgebras.

There is no assumption that , that is nonzero or separable, or that a representation has been chosen.

The same is commutative, inclusion-maximal among commutative unital -subalgebras, and contains the specified .

Self-adjointness supplies normality; apply the normal-element containment theorem, whose maximality comes from Zorn’s lemma.

Proof steps

Self-adjointness gives , so is normal. The normal-element theorem Maximal abelian containment for a normal element therefore applies to this . Its starting subalgebra is the closed unital -subalgebra ; normality makes commutative and .
Consider all commutative unital -subalgebras containing , ordered by inclusion. This set is nonempty because it contains . A nonempty chain has the union as its algebraic star-subalgebra upper bound: finitely many elements needed in an algebra operation lie together in one chain member, and any two elements commute there. This is the directed supremum used in the source. An empty chain is bounded by . Zorn’s lemma gives a maximal such .
If a commutative unital -subalgebra contains , then it also contains , so the maximality just obtained forces . Thus is maximal abelian in the full sense, and . The separate result Maximal abelianness implies norm closedness also gives norm closedness: is a commutative -subalgebra containing , so maximality forces .

theorem exists_maximalAbelian_containing_isSelfAdjoint
    (x : A) (hx : IsSelfAdjoint x) :
    ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D

In the source	Mathematical meaning
`(x : A)`	The specified element of the unital complex -algebra .
`(hx : IsSelfAdjoint x)`	The equation .
`∃ D : StarSubalgebra ℂ A`	One unital complex -subalgebra is chosen.
`IsMaximalAbelian D`	That is commutative, and every commutative unital -subalgebra containing it equals it.
`∧ x ∈ D`	The same contains the original specified element .

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

Accepted content SHA-256: 4007241b8b41a75aecfb90d6352938b6fbc7840c442ba2a4b54d65efb8d21036

Accepted source guide SHA-256: 942e71b04060f1f9f5327973b33a3653c2ff053069c998400519edb0081e7edf

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73