MATHLIBANNEX / CANONICAL DECLARATION CARD

Maximal abelian -subalgebras

MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian

def

Defines maximality by inclusion among commutative unital -subalgebras.

Statement

Let be a unital complex -algebra and let be a unital complex -subalgebra. The predicate below says that is commutative and that no strictly larger commutative unital -subalgebra contains it.

Definition

Explicitly, is maximal abelian precisely when both conditions hold: and, for every commutative unital -subalgebra , In the second condition the two inclusions force . The comparison is with all such subalgebras, not only with norm-closed ones.

Assumptions

contains the unit and is closed under addition, complex scalar multiplication, multiplication and adjoints. Norm closedness is not an assumption in this definition.

Conclusion

This is a property of the given subalgebra , rather than a construction of a new subalgebra.

Norm closedness of a maximal abelian subalgebra is a later consequence, not an extra conjunct of this predicate.

Main citations

Lean source signature (exact)

The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.

/-- A maximal abelian unital star subalgebra, expressed without installing a
global commutative-ring instance on its subtype. -/
def IsMaximalAbelian (D : StarSubalgebra ℂ A) : Prop :=
  IsMulCommutative D ∧
    ∀ E : StarSubalgebra ℂ A, IsMulCommutative E → D ≤ E → E ≤ D
In the source Mathematical meaning
D : StarSubalgebra ℂ A The specified unital complex -subalgebra of .
: Prop The output is a condition that may or may not hold for .
IsMulCommutative D For any two elements of , their products satisfy .
∀ E : StarSubalgebra ℂ A Quantify over every unital complex -subalgebra of the same .
IsMulCommutative E → D ≤ E → E ≤ D If is commutative and contains , then every element of already lies in ; hence .

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

Accepted content SHA-256: bb1f3ebea0dfdd93940e59ced9c7e7c34734baef551a6372097567c1684d4e2f

Accepted source guide SHA-256: 3eb8b1349b03e9dbdda1322b99196ea48819775f7d4e9ac440d1a1ef15c077f0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑