The unitary group in a unital C⋆-algebra is locally path connected

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.

Main results

• unitary.argSelfAdjoint: the selfadjoint element obtained by taking the argument (using the principal branch and the continuous functional calculus) of a unitary. This returns 0 if the principal branch of the logarithm is not continuous on the spectrum of the unitary element.
• selfAdjoint.norm_sq_expUnitary_sub_one: ‖(selfAdjoint.expUnitary x - 1 : A)‖ ^ 2 = 2 * (1 - Real.cos ‖x‖)
• unitary.norm_argSelfAdjoint: ‖unitary.argSelfAdjoint u‖ = Real.arccos (1 - ‖(u - 1 : A)‖ ^ 2 / 2)
• unitary.openPartialHomeomorph: the maps unitary.argSelfAdjoint and selfAdjoint.expUnitary form a partial homeomorphism between ball (1 : unitary A) 2 and ball (0 : selfAdjoint A) π.
• selfAdjoint.expUnitaryPathToOne: the path t ↦ expUnitary (t • x) from 1 to expUnitary x for a selfadjoint element x.
• unitary.isPathConnected_ball: any ball of radius δ < 2 in the unitary group of a unital C⋆-algebra is path connected.
• unitary.instLocPathConnectedSpace: the unitary group of a C⋆-algebra is locally path connected.
• unitary.mem_pathComponentOne_iff: The path component of the identity in the unitary group of a C⋆-algebra is the set of unitaries that can be expressed as a product of exponentials of selfadjoint elements.

theorem unitary.two_mul_one_sub_le_norm_sub_one_sq {A : Type u_1} [CStarAlgebra A] {u : A} (hu : u ∈ unitary A) {z : ℂ} (hz : z ∈ spectrum ℂ u) : 2 * (1 - z.re) ≤ ‖u - 1‖ ^ 2

theorem unitary.norm_sub_one_sq_eq {A : Type u_1} [CStarAlgebra A] {u : A} (hu : u ∈ unitary A) {x : ℝ} (hz : IsLeast (Complex.re '' spectrum ℂ u) x) : ‖u - 1‖ ^ 2 = 2 * (1 - x)

theorem unitary.norm_sub_one_lt_two_iff {A : Type u_1} [CStarAlgebra A] {u : A} (hu : u ∈ unitary A) : ‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u

theorem unitary.spectrum_subset_slitPlane_iff_norm_lt_two {A : Type u_1} [CStarAlgebra A] {u : A} (hu : u ∈ unitary A) : spectrum ℂ u ⊆ Complex.slitPlane ↔ ‖u - 1‖ < 2

theorem IsSelfAdjoint.cfc_arg {A : Type u_1} [CStarAlgebra A] (u : A) : IsSelfAdjoint (cfc (Complex.ofReal ∘ Complex.arg) u)

noncomputable def unitary.argSelfAdjoint {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) : ↥(selfAdjoint A)

The selfadjoint element obtained by taking the argument (using the principal branch and the continuous functional calculus) of a unitary whose spectrum does not contain -1. This returns 0 if the principal branch of the logarithm is not continuous on the spectrum of the unitary element.

Equations

• unitary.argSelfAdjoint u = ⟨cfc (fun (x : ℂ) => ↑x.arg) ↑u, ⋯⟩

@[simp]

theorem unitary.argSelfAdjoint_coe {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) : ↑(argSelfAdjoint u) = cfc (fun (x : ℂ) => ↑x.arg) ↑u

theorem selfAdjoint.norm_sq_expUnitary_sub_one {A : Type u_1} [CStarAlgebra A] {x : ↥(selfAdjoint A)} (hx : ‖x‖ ≤ Real.pi) : ‖↑(expUnitary x) - 1‖ ^ 2 = 2 * (1 - Real.cos ‖x‖)

theorem argSelfAdjoint_expUnitary {A : Type u_1} [CStarAlgebra A] {x : ↥(selfAdjoint A)} (hx : ‖x‖ < Real.pi) : unitary.argSelfAdjoint (selfAdjoint.expUnitary x) = x

theorem expUnitary_argSelfAdjoint {A : Type u_1} [CStarAlgebra A] {u : ↥(unitary A)} (hu : ‖↑u - 1‖ < 2) : selfAdjoint.expUnitary (unitary.argSelfAdjoint u) = u

theorem unitary.norm_argSelfAdjoint_le_pi {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) : ‖argSelfAdjoint u‖ ≤ Real.pi

theorem unitary.two_mul_one_sub_cos_norm_argSelfAdjoint {A : Type u_1} [CStarAlgebra A] {u : ↥(unitary A)} (hu : ‖↑u - 1‖ < 2) : 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = ‖↑u - 1‖ ^ 2

theorem unitary.norm_argSelfAdjoint {A : Type u_1} [CStarAlgebra A] {u : ↥(unitary A)} (hu : ‖↑u - 1‖ < 2) : ‖argSelfAdjoint u‖ = Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2)

theorem unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hu : ‖↑u - 1‖ < 2) : ‖↑(selfAdjoint.expUnitary (t • argSelfAdjoint u)) - 1‖ ≤ ‖↑u - 1‖

theorem unitary.continuousOn_argSelfAdjoint {A : Type u_1} [CStarAlgebra A] : ContinuousOn argSelfAdjoint (Metric.ball 1 2)

noncomputable def unitary.openPartialHomeomorph {A : Type u_1} [CStarAlgebra A] : OpenPartialHomeomorph ↥(unitary A) ↥(selfAdjoint A)

the maps unitary.argSelfAdjoint and selfAdjoint.expUnitary form a partial homeomorphism between ball (1 : unitary A) 2 and ball (0 : selfAdjoint A) π.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem unitary.openPartialHomeomorph_source {A : Type u_1} [CStarAlgebra A] : openPartialHomeomorph.source = Metric.ball 1 2

@[simp]

theorem unitary.openPartialHomeomorph_apply {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) : ↑openPartialHomeomorph u = argSelfAdjoint u

@[simp]

theorem unitary.openPartialHomeomorph_symm_apply {A : Type u_1} [CStarAlgebra A] (a : ↥(selfAdjoint A)) : ↑openPartialHomeomorph.symm a = selfAdjoint.expUnitary a

@[simp]

theorem unitary.openPartialHomeomorph_target {A : Type u_1} [CStarAlgebra A] : openPartialHomeomorph.target = Metric.ball 0 Real.pi

theorem unitary.norm_sub_eq {A : Type u_1} [CStarAlgebra A] (u v : ↥(unitary A)) : ‖↑u - ↑v‖ = ‖↑(u * star v) - 1‖

theorem unitary.expUnitary_eq_mul_inv {A : Type u_1} [CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑u - ↑v‖ < 2) : selfAdjoint.expUnitary (argSelfAdjoint (u * star v)) = u * star v

noncomputable def selfAdjoint.expUnitaryPathToOne {A : Type u_1} [CStarAlgebra A] (x : ↥(selfAdjoint A)) : Path 1 (expUnitary x)

For a selfadjoint element x in a C⋆-algebra, this is the path from 1 to expUnitary x given by t ↦ expUnitary (t • x).

Equations

• selfAdjoint.expUnitaryPathToOne x = { toFun := fun (t : ↑unitInterval) => selfAdjoint.expUnitary (↑t • x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem selfAdjoint.expUnitaryPathToOne_apply {A : Type u_1} [CStarAlgebra A] (x : ↥(selfAdjoint A)) (t : ↑unitInterval) : (expUnitaryPathToOne x) t = expUnitary (↑t • x)

@[simp]

theorem selfAdjoint.joined_one_expUnitary {A : Type u_1} [CStarAlgebra A] (x : ↥(selfAdjoint A)) : Joined 1 (expUnitary x)

noncomputable def unitary.path {A : Type u_1} [CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑v - ↑u‖ < 2) : Path u v

The path t ↦ expUnitary (t • argSelfAdjoint (v * star u)) * u from u : unitary A to v when ‖v - u‖ < 2.

Equations

• unitary.path u v huv = { toFun := fun (t : ↑unitInterval) => selfAdjoint.expUnitary (↑t • unitary.argSelfAdjoint (v * star u)) * u, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem unitary.path_apply {A : Type u_1} [CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑v - ↑u‖ < 2) (t : ↑unitInterval) : (path u v huv) t = selfAdjoint.expUnitary (↑t • argSelfAdjoint (v * star u)) * u

theorem unitary.joined {A : Type u_1} [CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑v - ↑u‖ < 2) : Joined u v

Two unitary elements u and v in a unital C⋆-algebra are joined by a path if the distance between them is less than 2.

theorem unitary.isPathConnected_ball {A : Type u_1} [CStarAlgebra A] (u : ↥(unitary A)) (δ : ℝ) (hδ₀ : 0 < δ) (hδ₂ : δ < 2) : IsPathConnected (Metric.ball u δ)

Any ball of radius δ < 2 in the unitary group of a unital C⋆-algebra is path connected.

instance unitary.instLocPathConnectedSpace {A : Type u_1} [CStarAlgebra A] : LocPathConnectedSpace ↥(unitary A)

The unitary group in a C⋆-algebra is locally path connected.

theorem unitary.mem_pathComponentOne_iff {A : Type u_1} [CStarAlgebra A] {u : ↥(unitary A)} : u ∈ pathComponent 1 ↔ ∃ (l : List ↥(selfAdjoint A)), (List.map selfAdjoint.expUnitary l).prod = u

The path component of the identity in the unitary group of a C⋆-algebra is the set of unitaries that can be expressed as a product of exponential unitaries.