Documentation

TauCeti.Geometry.Lie.Adjoint.Derivation

The adjoint action on left-invariant derivations #

The tangent adjoint action is transported across the canonical Lie equivalence between the tangent space at the identity and left-invariant derivations. The result is the roadmap-facing group adjoint Ad on Mathlib's Lie algebra LeftInvariantDerivation I G.

The canonical derivation–tangent equivalence uses Hausdorffness to identify point derivations with tangent vectors through global smooth functions. This imposes no extra public hypothesis on Ad or its group laws: a charted space over the normed model is T1, and a T1 topological group is Hausdorff. No boundaryless manifold assumption is needed, because a Lie group's identity is automatically an interior point.

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

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.Lie.Ad {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] (g : G) :
LeftInvariantDerivation I G ≃ₗ⁅ℝ⁆ LeftInvariantDerivation I G

The group adjoint on left-invariant derivations, obtained by transporting the differential of conjugation across evaluation at the identity.

Instances For
    source
    theorem TauCeti.Lie.Ad_apply {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] (g : G) (D : LeftInvariantDerivation I G) :
    (Ad g) D = (leftInvariantDerivationLieEquivGroupLieAlgebra ⋯).symm ((tangentAd g) ((leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) D))

    Applying the derivation adjoint is applying the tangent adjoint through the canonical Lie equivalence.

    source
    @[simp]
    theorem TauCeti.Lie.leftInvariantDerivationLieEquivGroupLieAlgebra_Ad {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] (g : G) (D : LeftInvariantDerivation I G) :
    (leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) ((Ad g) D) = (tangentAd g) ((leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) D)

    Evaluation at the identity intertwines the derivation and tangent adjoint actions.

    source
    @[simp]
    theorem TauCeti.Lie.leftInvariantDerivationLieEquivGroupLieAlgebra_symm_mfderiv_conjDiffeomorph {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] (g : G) (a : GroupLieAlgebra I G) :
    (leftInvariantDerivationLieEquivGroupLieAlgebra ⋯).symm ((mfderiv% ⇑(conjDiffeomorph g) 1) a) = (Ad g) ((leftInvariantDerivationLieEquivGroupLieAlgebra ⋯).symm a)

    The inverse tangent identification intertwines the tangent and derivation adjoint actions.

    source
    @[simp]
    theorem TauCeti.Lie.leftInvariantDerivationLinearIsometryEquivModelVectorSpace_Ad {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] (g : G) (D : LeftInvariantDerivation I G) :
    have x := ⋯; have x_1 := ⋯; leftInvariantDerivationLinearIsometryEquivModelVectorSpace ((Ad g) D) = (tangentAd g) (leftInvariantDerivationLinearIsometryEquivModelVectorSpace D)

    The canonical isometric identification with the model space intertwines the derivation and tangent adjoint actions.

    source
    @[simp]
    theorem TauCeti.Lie.Ad_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] :
    Ad 1 = LieEquiv.refl

    The identity element acts trivially on left-invariant derivations.

    source
    @[simp]
    theorem TauCeti.Lie.Ad_mul {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] (g h : G) :
    Ad (g * h) = (Ad h).trans (Ad g)

    A product acts by the composite of the two derivation adjoint automorphisms.

    source
    @[simp]
    theorem TauCeti.Lie.Ad_inv {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] (g : G) :
    Ad g⁻¹ = (Ad g).symm

    The adjoint of an inverse is the inverse adjoint automorphism.