The geometric structure family is the family of extreme-functional kernels

MathlibAnnex.Analysis.CStarAlgebra.geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall

theorem

Identifies the geometric structure family with kernels of extreme dual functionals.

Statement

Let be a complex C*-algebra, with no identity required. Write for the space of bounded complex-linear functionals on and for its closed unit ball. For a maximal proper face of the algebra unit ball , let

\Sigma(F)=\{\rho\in A^*:\|\rho\|\le1,\ \rho(a)=1\text{ for all }a\in F\},\qquad I_F=\bigcup_{\rho\in\Sigma(F)}\ker\rho.

For these nonempty unit-ball faces, the support-functional norm theorem identifies with the norm-one linear functionals supporting . The original geometric structure family is , a family of subsets of . Then

\mathcal S_A =\{\ker\rho:\rho\in\operatorname{ext}_{\mathbb R}(B_{A^*})\}. \tag{1}

Thus the points of the geometric structure space , originally defined from maximal faces and all their supporting kernels, are exactly these extreme-functional kernels.

Assumptions

Faces use the underlying real convex structure, while every functional and every kernel in (1) is complex-linear on the full algebra . The source uses the compatible C*-order. Nontriviality excludes the zero algebra, where the original face family is empty but the dual ball has the extreme point zero. No change to the original definition of is part of the assertion.

Conclusion

Formula (1) is equality of families of subsets, with both inclusions. Repeated kernels represent one point. No injectivity of the kernel parametrization, and no equality between a functional kernel and a representation kernel, is asserted.

Main citations

Exact family equality: geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall.
Maximal faces and their full support singleton: the separate facial and support statements.
The original family definition and supporting-kernel union: the objects on the left side of (1).
ExtremeKernel.lean, supportKernelUnion_unitBallSupportFace_eq_ker: the separate union-of-supporting-kernels identity.

Lean source signature (exact)

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

theorem geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall :
    NormedSpace.geometricStructureFamily ℂ A =
      (fun rho : StrongDual ℂ A => (rho.ker : Set A)) ''
        (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ

Back to the reading-guide item

In the source	Mathematical meaning
Algebra and order`variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A] variable [PartialOrder A] [StarOrderedRing A]`Fixed source	The nonzero complex C*-algebra and its compatible order. No identity is required.
Original geometric family`theorem geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall : NormedSpace.geometricStructureFamily ℂ A =`Fixed source	The left side is the previously defined family of subsets of , obtained from maximal proper faces and all their supporting kernels.
Kernel map and its image`(fun rho : StrongDual ℂ A => (rho.ker : Set A)) '' (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ := by`Fixed source	The function sends a bounded complex-linear functional to its kernel as a subset of . Its image is taken over the real extreme points of the closed dual unit ball: $\{\ker\rho:\rho\in\operatorname{ext}_{\mathbb R}(B_{A^*})\}.$ The equality in (1) identifies this entire family with ; it does not assert injectivity of the kernel map.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

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

Back to the reading-guide item

Exact surrounding source:

variable [PartialOrder A] [StarOrderedRing A]

Back to the reading-guide item

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

Technical documentation