Projection-supremum transport

This module relates the inherited operator order on projections in concrete star subalgebras to multiplication, then transports projection suprema across star-algebra equivalences. It supplies the normality witness consumed by the spatial factor equivalence in Zhou §3.

theorem Connes.StarSubalgebra.le_iff_mul_eq_left_of_isStarProjection {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : StarSubalgebra ℂ (E →L[ℂ] E)} {p q : ↥A} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p * q = p

The inherited operator order agrees with the algebraic order on star-subalgebra projections.

@[simp]

theorem Connes.StarAlgEquiv.map_le_map_iff_of_isStarProjection {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {A : StarSubalgebra ℂ (E →L[ℂ] E)} {B : StarSubalgebra ℂ (F →L[ℂ] F)} (e : ↥A ≃⋆ₐ[ℂ] ↥B) {p q : ↥A} (hp : IsStarProjection p) (hq : IsStarProjection q) : e p ≤ e q ↔ p ≤ q

A star-algebra equivalence preserves operator order between subalgebra projections.

theorem Connes.IsProjectionSupremum.map_starAlgEquiv {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {A : StarSubalgebra ℂ (E →L[ℂ] E)} {B : StarSubalgebra ℂ (F →L[ℂ] F)} (e : ↥A ≃⋆ₐ[ℂ] ↥B) {S : Set ↥A} {p : ↥A} (hp : IsProjectionSupremum S p) : IsProjectionSupremum (⇑e '' S) (e p)

A star-algebra equivalence carries a projection supremum to its image.

theorem Connes.StarAlgEquiv.isNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {A : StarSubalgebra ℂ (E →L[ℂ] E)} {B : StarSubalgebra ℂ (F →L[ℂ] F)} (e : ↥A ≃⋆ₐ[ℂ] ↥B) : IsNormalStarAlgEquiv e

Every star-algebra equivalence between operator subalgebras preserves projection suprema.