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.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
    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) :
    (hfdifferential (_ : (smoothLeftMul I g) 1 = g)) ((Derivation.evalAt 1) X) = (Derivation.evalAt g) X

    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
    • One or more equations did not get rendered due to their size.
    Equations
    • LeftInvariantDerivation.instInhabitedLeftInvariantDerivation = { default := 0 }
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    @[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
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    @[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
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      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 𝕜 ) :
        Equations
        • One or more equations did not get rendered due to their size.
        @[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
        • One or more equations did not get rendered due to their size.