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 #
@[simp]
theorem
selfAdjoint.expUnitary_coe
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
(a : ↥(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 : ↥(selfAdjoint A))
:
↥(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), ⋯⟩
Instances For
theorem
Commute.expUnitary_add
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
{a : ↥(selfAdjoint A)}
{b : ↥(selfAdjoint A)}
(h : Commute ↑a ↑b)
:
theorem
Commute.expUnitary
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
{a : ↥(selfAdjoint A)}
{b : ↥(selfAdjoint A)}
(h : Commute ↑a ↑b)
: