A coefficient-kernel component equals the normal part

MathlibAnnex.Analysis.CStarAlgebra.component_restrictedMatrixCoefficientKernel_eq_normalPart

theorem

Identifies the normal part with one component of the ambient geometric structure space.

Statement

Let be a complex Hilbert space, and let be a nonzero norm-closed complex -subalgebra acting irreducibly on . No identity is required. For , define the bounded linear functional

f_{x,y}:A\to\mathbb C,\qquad f_{x,y}(a)=\langle y,a(x)\rangle,

where the inner product is conjugate-linear in the first variable. The geometric structure space consists of the kernels of extreme points of the closed unit ball of the Banach dual of , with convexity over . The coefficient-kernel membership theorem guarantees that every above belongs to . For , the hull–kernel closure is

c_A(D)=\left\{I\in S(A):\bigcap_{J\in D}J\subseteq I\right\}.

Two points are linked if they are equal or their two-point set is not closed. For , let be its component under finite chains of links, including itself. Then, for every ,

C(\ker f_{x,y})=N(A)=\left\{\ker f_{z,w}:z,w\in H\setminus\{0\}\right\}. \tag{1}

The set is called the normal part of .

Assumptions

The algebra has its inherited operator norm and adjoint. Here irreducibility means that the only closed -invariant subspaces of are and ; nonzero action is ensured by . The vectors need not be unit vectors.

Conclusion

Thus is one component of the ambient space , independent of the nonzero pair used to specify the starting kernel. This does not assert .

Main citations

The normal-part definition: the membership condition with a single nonzero pair.
Whole-component theorem: component_matrixCoefficientKernel_eq_family, the result retained from the preceding component analysis.
Exact concrete component theorem: the equality for the inclusion representation.
arXiv:2504.05551v1, Lemma 6.3 and Definition 6.4: the coefficient component and the normal-part terminology.

Lean source signature (exact)

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

theorem component_restrictedMatrixCoefficientKernel_eq_normalPart
    (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))
    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :
    (NormedSpace.geometricStructureClosure ℂ S).component
      (restrictedMatrixCoefficientKernel S hS x y hx hy) = normalPart S

Back to the reading-guide item

In the source, S denotes the algebra used here.

In the source	Mathematical meaning
Hilbert space`variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`Fixed source	The complete complex Hilbert space on which acts.
Closed operator algebra`variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (S : Set (H →L[ℂ] H))]`Fixed source	The source name denotes the algebra . The closedness assumption concerns this subset of bounded operators.
Inherited C*-algebra structure`private abbrev normalPartCStarAlgebra : NonUnitalCStarAlgebra S := NonUnitalStarSubalgebra.nonUnitalCStarAlgebra S (h_closed := inferInstance) attribute [local instance] normalPartCStarAlgebra`Fixed source	The closed subalgebra has the inherited C*-algebra structure. The local instance makes that structure available when forming and its closure; it does not impose a new hypothesis.
Irreducibility and coefficient vectors`(hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :`Fixed source	The inclusion action of is nonzero and irreducible. The two vectors are , defining in (1).
Ambient component equality`(NormedSpace.geometricStructureClosure ℂ S).component (restrictedMatrixCoefficientKernel S hS x y hx hy) = normalPart S := by`Fixed source	The complete starting point is the coefficient kernel for the same . The component is taken in the ambient space , and $C(\ker f_{x,y})=N(A).$ It is not a component formed after restricting to , and it does not assert .
Coefficient-kernel point`def restrictedMatrixCoefficientKernel (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) : NormedSpace.GeometricStructureSpace ℂ S := ⟨{a : S \| inner ℂ y ((a : H →L[ℂ] H) x) = 0}, setOf_inner_apply_eq_zero_mem_geometricStructureFamily S hS x y hx hy⟩`Fixed source	The constructed point has underlying subset ; the stated irreducibility and nonzero-vector conditions certify its membership in . The coefficient-kernel evaluation records that same subset.
Normal part`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}`Fixed source	The set consists of geometric points for which there exist with . Under the present hypotheses every such kernel is a geometric point, as used in (1).

The local instance below is a consequence of the closed-subalgebra hypothesis. The following Image section and its new variables are not part of this theorem.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

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

Back to the reading-guide item

Exact surrounding source:

variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (S : Set (H →L[ℂ] H))]

Back to the reading-guide item

Exact surrounding source:

private abbrev normalPartCStarAlgebra : NonUnitalCStarAlgebra S :=
  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra S (h_closed := inferInstance)

attribute [local instance] normalPartCStarAlgebra

Back to the reading-guide item

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

Technical documentation