Maximal abelian star subalgebra

MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian

def

Defines maximal abelian unital star subalgebras by commutativity and maximality under inclusion.

Statement

Let D be a unital star subalgebra of a unital complex C*-algebra A. D is commutative, and any commutative unital star subalgebra E containing D is contained in D; thus D is maximal for inclusion among such subalgebras.

Definition

IsMaximalAbelian D ↔ IsMulCommutative D ∧ ∀ E, IsMulCommutative E → D ≤ E → E ≤ D.

Assumptions

Let D be a unital star subalgebra of a unital complex C*-algebra A.

Conclusion

D is commutative, and any commutative unital star subalgebra E containing D is contained in D; thus D is maximal for inclusion among such subalgebras.

Main citations

Lean source signature (exact)

def IsMaximalAbelian (D : StarSubalgebra ℂ A) : Prop

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