Commit 2025-10-14 23:42 4c492e56

feat: the unitary group in a C⋆-algebra is locally path connected (#30311) When A is a unital C⋆-algebra and u : unitary A is a unitary element whose distance to 1 is less that 2, the spectrum of u is contained in the slit plane, so the principal branch of the logarithm is continuous on the spectrum of u (or equivalently, Complex.arg is continuous on the spectrum). The continuous functional calculus can then be used to define a selfadjoint element x such that u = exp (I • x). Moreover, there is a relatively nice relationship between the norm of x and the norm of u - 1, namely ‖u - 1‖ ^ 2 = 2 * (1 - cos ‖x‖). In fact, these maps u ↦ x and x ↦ u establish a partial homeomorphism between ball (1 : unitary A) 2 and ball (0 : selfAdjoint A) π. The map t ↦ exp (t • (I • x)) constitutes a path from 1 to u, showing that unitary elements sufficiently close (i.e., within a distance 2) to 1 : unitary A are path connected to 1. This property can be translated around the unitary group to show that if u v : unitary A are unitary elements with ‖u - v‖ < 2, then there is a path joining them. In fact, this path has the property that it lies within closedBall u ‖u - v‖, and consequently any ball of radius δ < 2 in unitary A is path connected. Therefore, the unitary group is locally path connected. Finally, we provide the standard characterization of the path component of 1 : unitary A as finite products of exponential unitaries.