MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner
theorem
Constructs a projection in the original algebra from an isolated non-scalar character of a unitization subalgebra.
Statement
Let be a nonzero complex -algebra, with no unit assumed. Let be a separable complex Hilbert space, and let be a nonzero irreducible representation representing the unique unitary-equivalence class of nonzero irreducible representations of . There is with
Assumptions
Separability is imposed on . The algebra need not be unital or separable. The scalar may depend on , while the projection is fixed.
Conclusion
The same nonzero star projection has a one-dimensional algebraic corner .
Proof route
Find an isolated character away from the scalar character, take its characteristic-function projection, show that its scalar coordinate vanishes, and extend its scalar corner from the abelian subalgebra to the ambient algebra.
Proof steps
Write , , and . Choose in and put . In the unitization , its image is self-adjoint. Apply Maximal abelian containment to obtain a maximal abelian unital -subalgebra containing . It is closed and commutative. The character countability theorem Countability of this character space applies to the given singleton , separable , and this closed .
The element is nonzero and has scalar coordinate zero. Together with countability, these are the inputs to An isolated non-scalar character, yielding an isolated character . Its singleton is both open and closed in the character space. Thus the continuous function corresponds under the Gelfand transform to a nonzero projection satisfying
That characteristic function is zero at the different character , so . This value is precisely the scalar coordinate of . Therefore for an element . Injectivity of transfers and to .
The ambient corner calculation is From maximal abelianness to a scalar ambient corner. For any , put . Since is commutative and , for we get
Maximal abelianness therefore puts in . Apply the earlier equation to this : . But makes , so .
Finally set for an arbitrary . With , the last equation is for . Injectivity of gives . This proves the universal scalar-corner condition on the same .
Main citations
Lean source signature (exact)
theorem exists_nonzero_projection_scalar_corner [Nontrivial A]
[TopologicalSpace.SeparableSpace H]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
∀ a : A, ∃ c : ℂ, p * a * p = c • p| In the source | Mathematical meaning |
|---|---|
[Nontrivial A] |
The algebra is nonzero: . This condition does not say whether a unit is assumed; that information comes from the surrounding -algebra structure. |
[TopologicalSpace.SeparableSpace H] |
Separability of the representation space, used to count characters. |
(pi : NonUnitalCStarRepresentation A H) |
The specified -representation ; no unit-preservation equation is required. |
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) |
The specified representation is nonzero irreducible, and every nonzero irreducible -representation of the same algebra is unitarily equivalent to it. |
∃ p : A |
One element is obtained in itself, after the unitization projection has zero scalar coordinate. |
IsStarProjection p |
That element satisfies both and . |
p ≠ 0 |
The same projection is nonzero. |
∀ a : A, ∃ c : ℂ, p * a * p = c • p |
For each algebra element choose a complex scalar , possibly depending on , so that the entire compressed product is . |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner
Accepted content SHA-256: dcaf42b5945566594f86facd75e382759ea6f580cd84fe37632b000407fb93ce
Accepted source guide SHA-256: 780f02453443ee88ac9e0467fbb4f41a71cdd51d0bcceb34bea04c408523d2cc
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73