MathlibAnnex.Analysis.CStarAlgebra.normalPartProjectivizationEquiv
def
Parametrizes the normal part by an ordered pair of complex projective lines.
Statement
Let be a norm-closed complex -subalgebra with nonzero irreducible inclusion representation on the complete complex Hilbert space . No identity is required. Let denote its set of one-dimensional complex linear subspaces and for . For , define by , with inner product conjugate-linear in the first variable, and let be the coefficient-kernel normal part of .
The definition gives a bijection
This is an equivalence of sets. It does not assert a homeomorphism for the usual product topology on the two projective spaces.
Definition
For two projective lines , choose their nonzero representatives . The defining map is
The representative-evaluation theorem gives the value for any nonzero representatives . The injectivity and surjectivity theorems make this map the bijection (1) under the stated hypotheses.
The inverse-evaluation theorem gives
Both formulas describe the same equivalence .
Assumptions
The algebra is closed in operator norm and its inclusion is nonzero irreducible. These hypotheses supply geometric coefficient points and recoverability of the two lines. No normalization, finite-dimensionality, separability, or dimension-at-least-two assumption is used. Each projective line is represented by a nonzero vector by definition.
Conclusion
A normal kernel determines one source line and one target line, and every pair of such lines determines one normal kernel. This gives coordinates on the existing normal part. Closure and linkedness remain separate structures; the linked-pair theorem identifies linkedness with agreement of one coordinate, not both.
Main citations
Projective equivalence and its defining results: the defining right-hand side and the preceding map, injectivity, and surjectivity results.
Equality of coefficient kernels and both vector lines: the separate irreducible-representation kernel equality result.
normalPartProjectivizationMap_mk: evaluation on any nonzero representatives.
normalPartProjectivizationEquiv_symm_point: inverse evaluation.
Lean source signature (exact)
The complete definition below is copied from the pinned source, including its defining right-hand side.
def normalPartProjectivizationEquiv : (ℙ ℂ H) × (ℙ ℂ H) ≃ normalPart S :=
Equiv.ofBijective (normalPartProjectivizationMap S hS)
⟨normalPartProjectivizationMap_injective S hS,
normalPartProjectivizationMap_surjective S hS⟩
In the source, S denotes the algebra used here.
| In the source | Mathematical meaning |
|---|---|
Exact declarationS, its closedness instance, and hS |
The closed concrete algebra in the text and nonzero irreducibility of its inclusion. These conditions ensure that all pairs used below yield normal kernels and that both lines are recoverable. |
Exact declaration(ℙ ℂ H) × (ℙ ℂ H) |
The ordered pair of source and target complex projective lines. This expression alone supplies no ordinary product-topology claim. |
Exact declaration≃ normalPart S |
A set-level bijection into the normal-part subtype, with an inverse on every such point. |
Exact declarationnormalPartProjectivizationMap S hS |
The representative map defining in (1); its evaluation on any nonzero is , not merely a formal label. |
Exact declarationEquiv.ofBijective with ..._injective and ..._surjective |
Injectivity and surjectivity of this very map, giving its inverse on every normal kernel. |
The next comment and attribute introduce a later evaluation theorem; they are not part of this defining right-hand side.
Exact surrounding source context (separate excerpts)
Source lines 27–30:
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))
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·