The geometric structure family is the family of pure-state translate kernels

MathlibAnnex.Analysis.CStarAlgebra.geometricStructureFamily_eq_setOf_exists_pureState_unitaryTranslate

theorem

Identifies geometric points with kernels of unitary translates of pure states.

Statement

Let be a complex C*-algebra, possibly without an identity. Let be its original geometric structure space: its points are the sets obtained as unions of the kernels of all norm-one bounded linear functionals supporting maximal proper faces of the closed unit ball. Write for the pure states of , that is, positive norm-one bounded complex-linear functionals that are extreme in that state space for real convexity.

For a unitary in the forced unitization , define . Then

S(A) =\{\ker(T_u\varphi):\varphi\in\mathcal P(A),\ u\in U(\widetilde A)\}. \tag{1}

Here denotes the unitization action on the original ideal ; the functional and its kernel in this formula are on .

Assumptions

The source requires the nonzero complex C*-algebra and its compatible order. Positivity and purity refer to functionals on ; the translating unitary is allowed to lie in its forced unitization. The kernel is complex-linear, even though the face and extreme-point conditions use real convexity. No positivity of the translated functional is required.

Conclusion

Every original geometric-structure point can be written using one pure state and one unitary, and every such pair gives a point. Formula (1) is a family equality, so two pairs with the same kernel give the same point. It does not assert uniqueness of a state–unitary pair or replace the original family by a new definition.

Main citations

Exact pure-state translate family equality: geometricStructureFamily_eq_setOf_exists_pureState_unitaryTranslate.
Extreme-kernel family and pure-state unitary decomposition: the related family equality and translation identities for the same pure state and unitary.
Ryotaro Tanaka, arXiv:2504.05551v1, Lemma 5.3: the paper's pure-state description of the geometric structure space.

Lean source signature (exact)

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

theorem geometricStructureFamily_eq_setOf_exists_pureState_unitaryTranslate :
    NormedSpace.geometricStructureFamily ℂ A =
      {I : Set A | ∃ phi : StrongDual ℂ A, IsPureNonUnitalState A phi ∧
        ∃ u : unitary (Unitization ℂ A), ((unitaryTranslate u phi).ker : Set A) = I}

In the source	Mathematical meaning
Exact declaration`{A : Type}`, the nonunital C-algebra, order and nontriviality instances	The common algebra and hypotheses of the two family descriptions.
Exact declaration`NormedSpace.geometricStructureFamily ℂ A`	The family of geometric-structure points, each a subset of obtained from a maximal face and its supporting functionals.
Exact declaration`{I : Set A \| ...}`	A family described by a property of the entire subset .
Exact declaration`∃ phi : StrongDual ℂ A, IsPureNonUnitalState A phi ∧ ...`	A pure state , with positivity, norm one and extremality as specified above.
Exact declaration`∃ u : unitary (Unitization ℂ A)`	One unitary of the forced unitization, for that same state. The state is the same one already quantified; the unitary is not required to belong to the original algebra.
Exact declaration`((unitaryTranslate u phi).ker : Set A) = I`	The equality , with the translated functional defined on .
The complete equalityExact declaration	Equality of families of subsets: every left member has the displayed witnesses, and every such pair gives a left member. No unique parametrization is asserted.

Exact surrounding source context (separate excerpts)

Source lines 25–25:

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

Source lines 26–26:

variable [PartialOrder A] [StarOrderedRing A]

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

Technical documentation