The exponential map from selfadjoint to unitary

In this file, we establish various properties related to the map fun a ↦ NormedSpace.exp ℂ A (I • a) between the subtypes selfAdjoint 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.

@[simp]

theorem selfAdjoint.expUnitary_coe {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A] [CompleteSpace A] [StarModule ℂ A] (a : { x : A // x ∈ selfAdjoint A }) : ↑(selfAdjoint.expUnitary a) = NormedSpace.exp ℂ (Complex.I • ↑a)

noncomputable def selfAdjoint.expUnitary {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A] [CompleteSpace A] [StarModule ℂ A] (a : { x : A // x ∈ selfAdjoint A }) : { x : A // x ∈ unitary A }

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

Equations

• selfAdjoint.expUnitary a = ⟨NormedSpace.exp ℂ (Complex.I • ↑a), ⋯⟩

theorem Commute.expUnitary_add {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A] [CompleteSpace A] [StarModule ℂ A] {a : { x : A // x ∈ selfAdjoint A }} {b : { x : A // x ∈ selfAdjoint A }} (h : Commute ↑a ↑b) : selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary a * selfAdjoint.expUnitary b

theorem Commute.expUnitary {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A] [CompleteSpace A] [StarModule ℂ A] {a : { x : A // x ∈ selfAdjoint A }} {b : { x : A // x ∈ selfAdjoint A }} (h : Commute ↑a ↑b) : Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)