Exponentiating the commutator operator

In a real Banach algebra, exponentiating the continuous commutator operator y ↦ x * y - y * x gives conjugation by exp x. This is the Banach-algebra shadow of the Lie-group identity Ad (lieExp X) = exp (ad X). The final result identifies the underlying linear map of the bounded commutator with Mathlib's LieAlgebra.ad for the associative-ring Lie bracket.

This advances Deliverable A, Layer 1 of TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.

Main definitions

• TauCeti.Lie.continuousCommutator: the continuous commutator operator associated to an algebra element.

Main results

• TauCeti.Lie.exp_mulLeft_apply: exponentiating left multiplication acts by exp x on the left.
• TauCeti.Lie.exp_mulRight_apply: the analogous right-multiplication identity.
• TauCeti.Lie.exp_mulLeft and TauCeti.Lie.exp_mulRight: the corresponding bounded-operator identities.
• TauCeti.Lie.exp_continuousCommutator_apply: its operator exponential acts by conjugation.
• TauCeti.Lie.exp_continuousCommutator: the corresponding equality of bounded operators.
• TauCeti.Lie.continuousCommutator_toLinearMap: its underlying linear map is Mathlib's LieAlgebra.ad.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".

@[simp]

theorem TauCeti.Lie.exp_mulLeft_apply {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x y : R) : (NormedSpace.exp ((ContinuousLinearMap.mul ℝ R) x)) y = NormedSpace.exp x * y

Exponentiating the bounded left-multiplication operator gives left multiplication by the algebra exponential.

@[simp]

theorem TauCeti.Lie.exp_mulRight_apply {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x y : R) : (NormedSpace.exp ((ContinuousLinearMap.mul ℝ R).flip x)) y = y * NormedSpace.exp x

Exponentiating the bounded right-multiplication operator gives right multiplication by the algebra exponential.

theorem TauCeti.Lie.exp_mulLeft {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : NormedSpace.exp ((ContinuousLinearMap.mul ℝ R) x) = (ContinuousLinearMap.mul ℝ R) (NormedSpace.exp x)

Exponentiating the bounded left-multiplication operator gives the operator of left multiplication by the algebra exponential.

theorem TauCeti.Lie.exp_mulRight {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : NormedSpace.exp ((ContinuousLinearMap.mul ℝ R).flip x) = (ContinuousLinearMap.mul ℝ R).flip (NormedSpace.exp x)

Exponentiating the bounded right-multiplication operator gives the operator of right multiplication by the algebra exponential.

noncomputable def TauCeti.Lie.continuousCommutator {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] : R →L[ℝ] R →L[ℝ] R

The continuous-linear family of endomorphisms y ↦ x * y - y * x.

Equations

• TauCeti.Lie.continuousCommutator = ContinuousLinearMap.mul ℝ R - (ContinuousLinearMap.mul ℝ R).flip

@[simp]

theorem TauCeti.Lie.continuousCommutator_apply {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] (x y : R) : (continuousCommutator x) y = x * y - y * x

@[simp]

theorem TauCeti.Lie.exp_continuousCommutator_apply {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x y : R) : (NormedSpace.exp (continuousCommutator x)) y = NormedSpace.exp x * y * NormedSpace.exp (-x)

Exponentiating the continuous commutator operator gives conjugation by the algebra exponential.

theorem TauCeti.Lie.exp_continuousCommutator {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : NormedSpace.exp (continuousCommutator x) = ((ContinuousLinearMap.mulLeftRight ℝ R) (NormedSpace.exp x)) (NormedSpace.exp (-x))

Exponentiating the continuous commutator gives the bounded conjugation operator.

theorem TauCeti.Lie.continuousCommutator_toLinearMap {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] (x : R) : ↑(continuousCommutator x) = (LieAlgebra.ad ℝ R) x

The continuous commutator is the bounded realization of Mathlib's algebraic adjoint map for the ring-commutator bracket supplied by LieRing.ofAssociativeRing. Callers who restate the right-hand side should enable that instance locally.