The exponential map from selfadjoint to unitary #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we establish various propreties related to the map λ a, exp ℂ A (I • a) between the subtypes self_adjoint A and unitary A.

TODO #

Show that any exponential unitary is path-connected in unitary A to 1 : unitary A.
Prove any unitary whose distance to 1 : unitary A is less than 1 can be expressed as an exponential unitary.
A unitary is in the path component of 1 if and only if it is a finite product of exponential unitaries.

source

@[simp]

theorem self_adjoint.exp_unitary_coe {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [has_continuous_star A] [complete_space A] [star_module ℂ A] (a : ↥(self_adjoint A)) :

↑(self_adjoint.exp_unitary a) = exp ℂ (complex.I • ↑a)

source

noncomputable def self_adjoint.exp_unitary {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [has_continuous_star A] [complete_space A] [star_module ℂ A] (a : ↥(self_adjoint A)) :

↥(unitary A)

The map from the selfadjoint real subspace to the unitary group. This map only makes sense over ℂ.

Equations

self_adjoint.exp_unitary a = ⟨exp ℂ (complex.I • ↑a), _⟩

source

theorem commute.exp_unitary_add {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [has_continuous_star A] [complete_space A] [star_module ℂ A] {a b : ↥(self_adjoint A)} (h : commute ↑a ↑b) :

self_adjoint.exp_unitary (a + b) = self_adjoint.exp_unitary a * self_adjoint.exp_unitary b

source

theorem commute.exp_unitary {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [has_continuous_star A] [complete_space A] [star_module ℂ A] {a b : ↥(self_adjoint A)} (h : commute ↑a ↑b) :

commute (self_adjoint.exp_unitary a) (self_adjoint.exp_unitary b)