Normality of the factor isomorphism [connes-001C]

✍️source

IsProjectionSupremumisNormal

L∃∀NAGENTDRAFTED

Zhou's Proposition 3.4 identifies the two group factors by combining Fourier transform with the fiber shear [zhou2026icc, Proposition 3.4]. The Lean development records two properties of the resulting star-algebra equivalence explicitly. Preservation of projection suprema in both directions follows automatically from the star-algebra equivalence between these concrete operator subalgebras, while preservation of the canonical trace is proved from the spatial unitary.

The definition Connes.IsProjectionSupremum says that \(p\) is a projection, every member of \(S\) is a projection below \(p\), and \(p\) lies below every projection that is an upper bound for \(S\). The last condition ranges only over projections, rather than all upper bounds as in the stronger ambient predicate IsLUB.

For star subalgebras of bounded operators, the usual order on projections is characterized by \(p\leq q\iff pq=p\). A star-algebra equivalence preserves multiplication, so Connes.IsProjectionSupremum.map_starAlgEquiv uses this characterization to preserve projection suprema. Applying the same argument to the equivalence and its inverse gives Connes.StarAlgEquiv.isNormal.

This refactor leaves the definitions of projection supremum and normal star-algebra equivalence independent of bounded operators. The operator order appears only in the theorem that applies those definitions to the group factors in Theorem [connes-0007].