Maximal faces of the C*-algebra unit ball and their unique support

MathlibAnnex.Analysis.CStarAlgebra.isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall

theorem

Characterizes maximal proper faces of a C*-algebra unit ball by extreme dual functionals.

Statement

Let be a complex C*-algebra, possibly without an identity, and let . Faces and convexity are taken over . We consider maximal proper faces of .

Write for the space of bounded complex-linear functionals on , with the operator norm. For , write

F_\rho=\{a\in B_A:\rho(a)=1\}.

For every subset ,

F\text{ is a maximal proper face of }B_A \quad\Longleftrightarrow\quad F=F_\rho\text{ for some }\rho\in\operatorname{ext}_{\mathbb R}(B_{A^*}). \tag{1}

The supporting condition is the complex equality . In the unit ball it is equivalent to the usual real supporting condition when .

Assumptions

The source fixes the C*-order on , which is used by the pure-state and interpolation inputs. Nontriviality is essential to the displayed equivalence: the zero algebra has no nonempty proper face, while its dual ball has the extreme point zero. No compactness of , identity in , or finite-dimensional assumption is imposed.

Conclusion

Equation (1) is the complete selected equivalence about subsets. The separately named theorem supportFunctionals_unitBallSupportFace_eq_singleton guarantees that the entire dual unit-ball support family of an extreme slice is the singleton containing that same extreme functional. existsUnique_extreme_support_of_isMaximalFace guarantees uniqueness. These are separate cited results, not extra conjuncts in the selected type.

Main citations

Exact equivalence: isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall.
Full support-family and unique-support results in the same module: weakStarSupportFunctionals_unitBallSupportFace_eq_singleton, supportFunctionals_unitBallSupportFace_eq_singleton, and existsUnique_extreme_support_of_isMaximalFace give the additional support and uniqueness guarantees just distinguished from (1).

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

theorem isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall (F : Set A) :
    NormedSpace.IsMaximalFace F ↔ ∃ rho : StrongDual ℂ A,
      rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ∧
        F = NormedSpace.unitBallSupportFace ℂ rho

In the source	Mathematical meaning
Exact declaration`{A : Type u}`, the C*-algebra, order and nontriviality instances	The nonzero complex C*-algebra with its compatible order. The real convex structure is obtained by restricting scalars.
Exact declaration`(F : Set A)`	An arbitrary subset of the original algebra, not a set of states or a subset of the self-adjoint part.
Exact declaration`NormedSpace.IsMaximalFace F`	Nonemptiness, real convexity, the face property in the norm-closed unit ball, properness, and maximality among proper convex faces.
Exact declaration`∃ rho : StrongDual ℂ A`	One continuous complex-linear supporting functional is chosen for the face.
Exact declaration`rho ∈ (closedBall ... 1).extremePoints ℝ`	The same is extreme for real convex combinations in the whole dual closed unit ball.
Exact declaration`F = NormedSpace.unitBallSupportFace ℂ rho`	Equality of the whole subset with . Together with extremality, this is the complete right side of the equivalence.
Exact declaration`↔` and the two conjuncts	Both directions hold, with one satisfying both conjuncts. Support-family uniqueness is a separately named result, not a field hidden inside `IsMaximalFace`.

Exact surrounding source context (separate excerpts)

Source lines 34–34:

variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]

Source lines 35–35:

variable [PartialOrder A] [StarOrderedRing A]

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation