Documentation

TauCeti.Geometry.Lie.Adjoint.Representation.Basic

The group adjoint representation #

This file bundles the group adjoint Ad as a continuous representation on left-invariant derivations. It transports operator-valued smoothness across the canonical isometric identification between left-invariant derivations and the tangent space at the identity, then derives joint smoothness of the action by evaluation.

Main definitions #

Main results #

source
theorem TauCeti.Lie.instFiniteDimensionalRealLeftInvariantDerivation_tauCeti {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] [T2Space G] :
FiniteDimensional ℝ (LeftInvariantDerivation I G)
source
noncomputable def TauCeti.Lie.continuousAdjointRepresentation {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] [T2Space G] :
ContRepresentation ℝ G (LeftInvariantDerivation I G)

The adjoint representation valued in bounded operators.

Instances For
    source
    @[simp]
    theorem TauCeti.Lie.continuousAdjointRepresentation_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] [T2Space G] (g : G) (D : LeftInvariantDerivation I G) :
    (continuousAdjointRepresentation g) D = (Ad g) D

    The packaged continuous adjoint representation acts by the derivation adjoint action.

    source
    theorem TauCeti.Lie.contMDiff_continuousAdjointRepresentation {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] [T2Space G] :
    ContMDiff I (modelWithCornersSelf ℝ (LeftInvariantDerivation I G →L[ℝ] LeftInvariantDerivation I G)) ↑⊤ ⇑continuousAdjointRepresentation

    The bounded-operator-valued adjoint representation is smooth.

    source
    theorem TauCeti.Lie.contMDiff_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] [T2Space G] :
    ContMDiff (I.prod (modelWithCornersSelf ℝ (LeftInvariantDerivation I G))) (modelWithCornersSelf ℝ (LeftInvariantDerivation I G)) ↑⊤ fun (p : G × LeftInvariantDerivation I G) => (Ad p.1) p.2

    The group adjoint action on left-invariant derivations is jointly smooth.