Maximal abelian subalgebra containing a self-adjoint element

MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

theorem

Places a self-adjoint element inside a maximal abelian unital star subalgebra.

Statement

Let x be self-adjoint in a unital complex C*-algebra A. There exists a maximal abelian unital star subalgebra D of A containing x.

Assumptions

Let x be self-adjoint in a unital complex C*-algebra A.

Conclusion

There exists a maximal abelian unital star subalgebra D of A containing x.

Proof route

The source turns self-adjointness into IsStarNormal x and applies exists_maximalAbelian_containing. Normality is an intermediate premise, not the theorem's conclusion.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian

  Exact formal dependency; inspect the linked Card and exact source.

Lean source signature (exact)

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

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