The differential of the adjoint representation #
The differential at the identity of the group adjoint representation is Mathlib's Lie-algebra adjoint map. This is the roadmap-facing form of the infinitesimal adjoint identity, stated on the canonical Lie algebra of left-invariant derivations.
This advances Deliverable A, Layer 1 of
TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.
Main results #
TauCeti.Lie.mfderiv_Ad_apply_one: the identityd(Ad)_1(X)(Y) = ad X Y.TauCeti.Lie.mfderiv_continuousAdjointRepresentation_one: the operator identityd(Ad)_1(X) = ad X.
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
@[simp]
theorem
TauCeti.Lie.mfderiv_Ad_apply_one
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
(X Y : LeftInvariantDerivation I G)
:
have x := ⋯;
(have this :=
((mfderiv% fun (g : G) => (Ad g) Y) 1)
((pointDerivationEquivTangentSpace 1 ⋯) ((LeftInvariantDerivation.evalAt 1) X));
this) = ((LieAlgebra.ad ℝ (LeftInvariantDerivation I G)) X) Y
The differential at the identity of the group adjoint action, evaluated on X and Y, is
the Lie-algebra adjoint ad X Y.
@[simp]
theorem
TauCeti.Lie.mfderiv_continuousAdjointRepresentation_one
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
(X : LeftInvariantDerivation I G)
:
have x := ⋯;
have x_1 := ⋯;
(have this :=
(mfderiv% ⇑continuousAdjointRepresentation 1)
((pointDerivationEquivTangentSpace 1 ⋯) ((LeftInvariantDerivation.evalAt 1) X));
this) = LinearMap.toContinuousLinearMap ((LieAlgebra.ad ℝ (LeftInvariantDerivation I G)) X)
The differential at the identity of the bounded-operator-valued adjoint representation is Mathlib's Lie-algebra adjoint map.