Linked normal kernels share a projective coordinate

MathlibAnnex.Analysis.CStarAlgebra.linked_normalPartPoint_iff_span_eq_or_span_eq

theorem

Characterizes linked normal kernels by agreement of one projective coordinate.

Statement

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

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

The inner product is conjugate-linear in its first variable. The normal part is . For , its inherited closure is

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

Two points are linked when they are equal or their two-point set is not closed for this closure. For ,

\ker f_{x_1,y_1}\text{ and }\ker f_{x_2,y_2}\text{ are linked} \quad\Longleftrightarrow\quad \mathbb Cx_1=\mathbb Cx_2\ \text{or}\ \mathbb Cy_1=\mathbb Cy_2. \tag{1}

Assumptions

All four vectors are nonzero, but no unit-length or linear-independence assumption is imposed. Under these hypotheses, the coefficient-kernel membership theorem guarantees that every nonzero pair defines a point of the normal part. The closure in (1) is restricted to , not to arbitrary points of the ambient geometric structure space.

Conclusion

One shared projective coordinate characterizes a linked pair. In contrast, the coefficient-kernel equality theorem identifies equality of the two points with agreement of both projective coordinates. Linkedness here is the original pair relation, not its finite-chain transitive closure.

Main citations

Linked-pair theorem: the equivalence (1), for the inherited normal-part closure.
arXiv:2504.05551v1, Lemma 6.10: the linkedness criterion in the normal part.

Lean source signature (exact)

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

theorem linked_normalPartPoint_iff_span_eq_or_span_eq
    (x₁ x₂ y₁ y₂ : H) (hx₁ : x₁ ≠ 0) (hx₂ : x₂ ≠ 0)
    (hy₁ : y₁ ≠ 0) (hy₂ : y₂ ≠ 0) :
    ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Linked
      (normalPartPoint S hS x₁ y₁ hx₁ hy₁) (normalPartPoint S hS x₂ y₂ hx₂ hy₂) ↔
      Submodule.span ℂ {x₁} = Submodule.span ℂ {x₂} ∨
      Submodule.span ℂ {y₁} = Submodule.span ℂ {y₂}

Back to the reading-guide item

In the source, S denotes the algebra used here.

In the source	Mathematical meaning
Hilbert space and irreducible algebra`variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) variable [IsClosed (S : Set (H →L[ℂ] H))] variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))`Fixed source	The complex Hilbert space and the nonzero norm-closed complex -subalgebra acting irreducibly. The source calls the algebra `S`.
Four nonzero vectors`(x₁ x₂ y₁ y₂ : H) (hx₁ : x₁ ≠ 0) (hx₂ : x₂ ≠ 0) (hy₁ : y₁ ≠ 0) (hy₂ : y₂ ≠ 0) :`Fixed source	The vectors belong to . There is no normalization or independence condition.
Linked coefficient kernels`((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Linked (normalPartPoint S hS x₁ y₁ hx₁ hy₁) (normalPartPoint S hS x₂ y₂ hx₂ hy₂) ↔`Fixed source	The two points are and in . The outer `subspace` gives the relative closure on . Linkedness means that the points are equal or that their two-point set is not closed; it does not mean a finite chain of links.
Projective source or target equality`Submodule.span ℂ {x₁} = Submodule.span ℂ {x₂} ∨ Submodule.span ℂ {y₁} = Submodule.span ℂ {y₂} := by`Fixed source	The two alternatives in (1) are $\mathbb Cx_1=\mathbb Cx_2\quad\text{or}\quad\mathbb Cy_1=\mathbb Cy_2.$ Each span is the complex line generated by its nonzero vector. The disjunction classifies linkedness; equality of the two kernels requires both line equalities, as stated in the separately cited result.

Linkedness includes equal points. The theorem concerns one linked pair, not a finite chain.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
variable [IsClosed (S : Set (H →L[ℂ] H))]
variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))

Back to the reading-guide item

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

Technical documentation