Structure forgetting and equivalence reuse [connes-000F]

✍️source

EquivariantHaarHomeomorphcontinuousCrossedClosure_mem_iff

L∃∀NAGENTDRAFTED

The formalization uses the topology of the fiber shear at an intermediate step. It defines the shear as an equivariant measure-preserving homeomorphism because pullback must preserve continuous coefficients. Once this density argument is complete, the crossed-product theorem uses only the underlying equivariant measurable equivalence.

Zhou's shear need not be additive, so the Lean proof does not treat it as a compact-group automorphism. Continuity is retained for the density argument and then forgotten. This matches the two roles separated in [zhou2026icc, Proposition 3.2 and Remark 3.3].

A second lesson came from the reverse inclusion between the generated operator algebras. Mathlib's continuous pullback is already a star-algebra equivalence, so its surjectivity proves that inclusion without a separate involutivity calculation. Similarly, the inverse law for conjugation by a linear isometry equivalence replaces a pointwise operator calculation. In both cases, an equality that first looked computational follows from the inverse laws of an equivalence.