Documentation

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Left invariant derivations #

In this file we define the concept of left invariant derivation for a Lie group. The concept is analogous to the more classical concept of left invariant vector fields, and it holds that the derivation associated to a vector field is left invariant iff the field is.

Moreover we prove that LeftInvariantDerivation I G has the structure of a Lie algebra, hence implementing one of the possible definitions of the Lie algebra attached to a Lie group.

structure LeftInvariantDerivation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] extends Derivation :
Type (max u_1 u_4)

Left-invariant global derivations.

A global derivation is left-invariant if it is equal to its pullback along left multiplication by an arbitrary element of G.

Instances For
    theorem LeftInvariantDerivation.left_invariant'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (self : LeftInvariantDerivation I G) (g : G) :
    (hfdifferential ) ((Derivation.evalAt 1) self) = (Derivation.evalAt g) self
    Equations
    • LeftInvariantDerivation.instCoeDerivationContMDiffMapModelWithCornersSelfTopENat = { coe := LeftInvariantDerivation.toDerivation }
    theorem LeftInvariantDerivation.toDerivation_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
    Function.Injective LeftInvariantDerivation.toDerivation
    Equations
    • LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfTopENat = { coe := fun (f : LeftInvariantDerivation I G) => f, coe_injective' := }
    theorem LeftInvariantDerivation.toFun_eq_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] {X : LeftInvariantDerivation I G} :
    (X).toFun = X
    theorem LeftInvariantDerivation.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
    Function.Injective DFunLike.coe
    theorem LeftInvariantDerivation.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] {X : LeftInvariantDerivation I G} {Y : LeftInvariantDerivation I G} (h : ∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ), X f = Y f) :
    X = Y
    theorem LeftInvariantDerivation.coe_derivation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) :
    X = X
    theorem LeftInvariantDerivation.left_invariant' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (g : G) (X : LeftInvariantDerivation I G) :

    Premature version of the lemma. Prefer using left_invariant instead.

    theorem LeftInvariantDerivation.map_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) {f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 } :
    X (f + f') = X f + X f'
    theorem LeftInvariantDerivation.map_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) :
    X 0 = 0
    theorem LeftInvariantDerivation.map_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) :
    X (-f) = -X f
    theorem LeftInvariantDerivation.map_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) {f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 } :
    X (f - f') = X f - X f'
    theorem LeftInvariantDerivation.map_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] {r : 𝕜} (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) :
    X (r f) = r X f
    @[simp]
    theorem LeftInvariantDerivation.leibniz {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) {f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 } :
    X (f * f') = f X f' + f' X f
    Equations
    • LeftInvariantDerivation.instZero = { zero := { toDerivation := 0, left_invariant'' := } }
    Equations
    • LeftInvariantDerivation.instInhabited = { default := 0 }
    Equations
    • LeftInvariantDerivation.instAdd = { add := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := X + Y, left_invariant'' := } }
    Equations
    • LeftInvariantDerivation.instNeg = { neg := fun (X : LeftInvariantDerivation I G) => { toDerivation := -X, left_invariant'' := } }
    Equations
    • LeftInvariantDerivation.instSub = { sub := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := X - Y, left_invariant'' := } }
    @[simp]
    theorem LeftInvariantDerivation.coe_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (Y : LeftInvariantDerivation I G) :
    (X + Y) = X + Y
    @[simp]
    theorem LeftInvariantDerivation.coe_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
    0 = 0
    @[simp]
    theorem LeftInvariantDerivation.coe_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) :
    (-X) = -X
    @[simp]
    theorem LeftInvariantDerivation.coe_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (Y : LeftInvariantDerivation I G) :
    (X - Y) = X - Y
    @[simp]
    theorem LeftInvariantDerivation.lift_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (Y : LeftInvariantDerivation I G) :
    (X + Y) = X + Y
    @[simp]
    theorem LeftInvariantDerivation.lift_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
    0 = 0
    Equations
    • LeftInvariantDerivation.hasNatScalar = { smul := fun (r : ) (X : LeftInvariantDerivation I G) => { toDerivation := r X, left_invariant'' := } }
    Equations
    • LeftInvariantDerivation.hasIntScalar = { smul := fun (r : ) (X : LeftInvariantDerivation I G) => { toDerivation := r X, left_invariant'' := } }
    Equations
    instance LeftInvariantDerivation.instSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
    Equations
    • LeftInvariantDerivation.instSMul = { smul := fun (r : 𝕜) (X : LeftInvariantDerivation I G) => { toDerivation := r X, left_invariant'' := } }
    @[simp]
    theorem LeftInvariantDerivation.coe_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (r : 𝕜) (X : LeftInvariantDerivation I G) :
    (r X) = r X
    @[simp]
    theorem LeftInvariantDerivation.lift_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (k : 𝕜) :
    (k X) = k X
    @[simp]

    The coercion to function is a monoid homomorphism.

    Equations
    Instances For
      instance LeftInvariantDerivation.instModule {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] :
      Equations

      Evaluation at a point for left invariant derivation. Same thing as for generic global derivations (Derivation.evalAt).

      Equations
      Instances For
        theorem LeftInvariantDerivation.evalAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (g : G) (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) :
        theorem LeftInvariantDerivation.comp_L {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (g : G) (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) :
        (X f).comp (smoothLeftMul I g) = X (f.comp (smoothLeftMul I g))
        Equations
        • LeftInvariantDerivation.instBracket = { bracket := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := X, Y, left_invariant'' := } }
        @[simp]
        theorem LeftInvariantDerivation.commutator_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (X : LeftInvariantDerivation I G) (Y : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ) :
        X, Y f = X (Y f) - Y (X f)
        Equations
        • LeftInvariantDerivation.instLieRing = LieRing.mk
        Equations