Maximal linked families are projective fibers

MathlibAnnex.Analysis.CStarAlgebra.maximal_isLinkedSet_normalPart_iff

theorem

Characterizes maximal linked subsets of the normal part as projective fibers.

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 by . The inner product is conjugate-linear in its first variable. The normal part is .

Let be the set of one-dimensional complex subspaces of , with for . The projective-coordinate equivalence is the bijection with , as given by its coefficient-kernel formula.

For , use the inherited closure . A set is pairwise linked if any two distinct members form a nonclosed two-point set. This is equivalent to requiring the linked relation, which also includes equality, for every pair of members. For define the source and target fibers

\mathcal R_p=\{e(p,t):t\in\mathbb P(H)\},\qquad \mathcal C_q=\{e(t,q):t\in\mathbb P(H)\}. \tag{1}

For any ,

\begin{aligned} L\text{ is maximal among pairwise-linked sets} \quad\Longleftrightarrow\quad & (\exists p\in\mathbb P(H),\ L=\mathcal R_p)\\ &\text{or }(\exists q\in\mathbb P(H),\ L=\mathcal C_q). \end{aligned} \tag{2}

Assumptions

Maximality is with respect to inclusion, among pairwise-linked subsets of the same normal part. There is no hypothesis that is closed, finite, or initially nonempty. The nonzero-action hypothesis excludes the zero Hilbert space. Dimension one is allowed; no lower bound of two is added.

Conclusion

Every maximal family fixes either the source projective line or the target projective line, and every fiber in (1) is maximal. The two descriptions need not be different: in dimension one both fibers are the whole singleton normal part. No uniqueness between the two alternatives of (2) is asserted.

Main citations

The projective-product bijection: every point has a unique ordered pair of projective coordinates.
The linked-pair criterion: two coefficient kernels are linked exactly when their source lines or their target lines agree.
Exact maximal-family theorem: the equivalence (2) for all subsets of the normal part.
arXiv:2504.05551v1, Definition 6.11 and Lemma 6.13: pairwise-linked sets and their maximal fibers; dimension one is included.

Lean source signature (exact)

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

theorem maximal_isLinkedSet_normalPart_iff (L : Set (normalPart S)) :
    Maximal
      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).IsLinkedSet L ↔
      (∃ p : ℙ ℂ H, L = normalPartSourceFiber S hS p) ∨
      (∃ q : ℙ ℂ H, L = normalPartTargetFiber S hS q)

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 source algebra `S` is the nonzero norm-closed complex -subalgebra acting irreducibly on the complex Hilbert space .
Set to be classified`theorem maximal_isLinkedSet_normalPart_iff (L : Set (normalPart S)) : Maximal ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).IsLinkedSet L ↔`Fixed source	The input is any subset of . It is maximal by inclusion among pairwise-linked subsets for the relative geometric closure on . Neither closedness of nor a greatest cardinality is required.
Pairwise linkedness`def IsLinkedSet (c : ClosureSpace α) (S : Set α) : Prop := ∀ x ∈ S, ∀ y ∈ S, c.Linked x y`Fixed source	The condition on is that every two of its points are linked for that closure. The `Maximal` in the preceding row also requires that no strictly larger subset has this property.
Source fiber`def normalPartSourceFiber (p : ℙ ℂ H) : Set (normalPart S) := {I \| ((normalPartProjectivizationEquiv S hS).symm I).1 = p}`Fixed source	The equivalence is from the Statement. The first coordinate of equals exactly on $\mathcal R_p=\{e(p,t):t\in\mathbb P(H)\}.$ Here `symm` denotes the inverse of that same .
Target fiber`def normalPartTargetFiber (q : ℙ ℂ H) : Set (normalPart S) := {I \| ((normalPartProjectivizationEquiv S hS).symm I).2 = q}`Fixed source	The second coordinate of equals exactly on $\mathcal C_q=\{e(t,q):t\in\mathbb P(H)\}.$ Both fibers use the same projective space and equivalence.
The two kinds of maximal family`(∃ p : ℙ ℂ H, L = normalPartSourceFiber S hS p) ∨ (∃ q : ℙ ℂ H, L = normalPartTargetFiber S hS q) := by`Fixed source	The conclusion is the disjunction $\bigl(\exists p\in\mathbb P(H),\ L=\mathcal R_p\bigr)\quad\text{or}\quad\bigl(\exists q\in\mathbb P(H),\ L=\mathcal C_q\bigr).$ It classifies all maximal linked families. The two kinds may coincide in dimension one; no dimension-at-least-two assumption is made.

The effective context requires nonzero irreducibility. There is no dimension-at-least-two or nonempty-family assumption.

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