The coefficient-kernel normal part — Exact Mathematics with AI

MathlibAnnex.Analysis.CStarAlgebra.normalPart

def

Defines the normal part by vector coefficient kernels that are geometric points.

Statement

Let be a complete complex Hilbert space and a complex -subalgebra, not required to contain an identity. Give the inherited operator norm. Its normal part selects those points of the geometric structure space of whose underlying subsets are kernels of vector coefficient functionals

f_{x,y}:A\longrightarrow\mathbb C,\qquad f_{x,y}(a)=\langle y,a(x)\rangle, \quad x,y\ne0. \tag{1}

The inner product is conjugate-linear in its first variable. This definition itself assumes neither norm-closedness nor irreducibility of .

Definition

For each maximal proper face of the closed unit ball of , take the union of the kernels of the norm-one bounded complex-linear functionals supporting . The geometric structure space is the family of these subsets, with repetitions identified. Faces use real convexity. The norm-one description follows from the support-functional norm theorem, since is a nonempty subset of the unit ball.

The normal part is the following subset of that already defined space:

N(A)=\left\{I\in S(A): \begin{array}{l} \text{there exist }x,y\in H\text{ with }x\ne0,\ y\ne0,\\ I=\ker f_{x,y} \end{array}\right\}. \tag{2}

In (2), the same pair satisfies both nonzero conditions and the kernel equality. With the stated inner-product convention, is complex-linear in .

The set (2) consists of points of that are coefficient kernels. For a general algebra , the kernel of a nonzero vector pair need not belong to . In particular, nonzero vectors alone need not make the restricted coefficient nonzero when the algebra is reducible. Under the additional closedness and irreducibility hypotheses in the component theorem, every nonzero pair does give a geometric point and the normal part is one entire component.

Assumptions

Only the complete complex Hilbert structure on and the complex -subalgebra structure on are required. Completeness or norm-closedness of , nonzero action, irreducibility, separability, and the existence of a unit in are not assumed.

Conclusion

The result is a subset of the geometric structure space, defined by literal equality with a vector coefficient's zero set. It is not a new quotient of pairs of vectors and does not yet assert a component equality, a projective parametrization, or a homeomorphism. Those statements require the additional hypotheses in the cited results.

Main citations

Exact normal-part definition: the set (2), before the later closedness binder.
The ambient geometric structure space: the original face-and-support construction used by the type in (2).
A coefficient-kernel component equals the normal part: the stronger conclusion for a closed irreducible concrete algebra.
arXiv:2504.05551v1, Definition 6.4: the normal part in the irreducible concrete setting. The general source definition is deliberately stated before those additional hypotheses.

Lean source signature (exact)

The complete definition below is copied from the pinned source, including its defining right-hand side.

def normalPart (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) :
    Set (NormedSpace.GeometricStructureSpace ℂ S) :=
  {I | ∃ x y : H, x ≠ 0 ∧ y ≠ 0 ∧
    {a : S | inner ℂ y ((a : H →L[ℂ] H) x) = 0} = I.val}

In the source, S denotes the algebra used here.

In the source	Mathematical meaning
Exact declaration`{H}` and the three Hilbert-space instances	The complete complex Hilbert space of (1). These conditions are on , not on the normed subalgebra .
Exact declaration`S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)`	The algebra in the text: a complex linear subspace of bounded complex-linear operators, closed under multiplication and adjoint; no unit-preservation or norm-closedness condition is part of this parameter.
Exact declaration`Set (NormedSpace.GeometricStructureSpace ℂ S)`	The normal part is a subset of the existing geometric space , whose points have underlying subsets of .
Exact declaration`∃ x y : H, x ≠ 0 ∧ y ≠ 0 ∧ ...`	One pair of vectors satisfies both nonzero conditions and the following equality. Separate pairs are not chosen for separate conjuncts.
Exact declaration`inner ℂ y ((a : H →L[ℂ] H) x) = 0` and `= I.val`	The entire coefficient zero set is the underlying subset of the same geometric point . The operator acts on and is paired against ; this is exactly (2).
The complete set-builder right-hand sideExact declaration	Selects only kernels that are already geometric points; component and projective claims require separate hypotheses and results.

No closedness or irreducibility binder is appended. The line immediately following this definition in the retained block is not part of its scope.

Exact surrounding source context (separate excerpts)

Source lines 32–32:

variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

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

Technical documentation