The differential of the exponential on a finite-dimensional algebra's units #
After coercing the units-valued Lie exponential to the ambient algebra, its Fréchet derivative is left multiplication by the exponential composed with the regularized commutator factor and the canonical identification of the abstract Lie algebra with the ambient algebra.
Main result #
TauCeti.Lie.fderiv_lieExp_units_coe_eq_exp_mul_banachDexpFactor: the bundled derivative formula.
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".
theorem
TauCeti.Lie.finiteDimensionalCompleteSpaceUnitsDexp
{R : Type u_1}
[NormedRing R]
[NormedAlgebra ℝ R]
[FiniteDimensional ℝ R]
:
theorem
TauCeti.Lie.finiteDimensionalLeftInvariantDerivationUnitsDexp
{R : Type u_1}
[NormedRing R]
[NormedAlgebra ℝ R]
[FiniteDimensional ℝ R]
:
theorem
TauCeti.Lie.fderiv_lieExp_units_coe_eq_exp_mul_banachDexpFactor
{R : Type u_1}
[NormedRing R]
[NormedAlgebra ℝ R]
[FiniteDimensional ℝ R]
(X : LeftInvariantDerivation (modelWithCornersSelf ℝ R) Rˣ)
:
fderiv ℝ (fun (Y : LeftInvariantDerivation (modelWithCornersSelf ℝ R) Rˣ) => ↑(lieExp Y)) X = (ContinuousLinearMap.mul ℝ R) (NormedSpace.exp (unitsLieAlgebraEquiv X)) ∘SL banachDexpFactor (unitsLieAlgebraEquiv X) ∘SL ↑unitsLieAlgebraEquiv.toContinuousLinearEquiv
The derivative of the units Lie exponential after coercion to the ambient algebra is left multiplication by the exponential composed with the regularized commutator factor and the canonical Lie-algebra equivalence.