# 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} {E : Type u_2} [] {H : Type u_3} [] (I : ) (G : Type u_4) [] [] [] [] extends :
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.

• toFun : ContMDiffMap I () G 𝕜 ContMDiffMap I () G 𝕜
• map_add' : ∀ (x y : ContMDiffMap I () G 𝕜 ), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (m : 𝕜) (x : ContMDiffMap I () G 𝕜 ), self.toFun (m x) = () m self.toFun x
• map_one_eq_zero' : self 1 = 0
• leibniz' : ∀ (a b : ContMDiffMap I () G 𝕜 ), self (a * b) = a self b + b self a
• left_invariant'' : ∀ (g : G), () ( self) = self
Instances For
Equations
• One or more equations did not get rendered due to their size.
theorem LeftInvariantDerivation.toDerivation_injective {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Function.Injective LeftInvariantDerivation.toDerivation
Equations
• One or more equations did not get rendered due to their size.
theorem LeftInvariantDerivation.toFun_eq_coe {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] {X : } :
X.toFun = X
theorem LeftInvariantDerivation.coe_injective {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Function.Injective DFunLike.coe
theorem LeftInvariantDerivation.ext {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] {X : } {Y : } (h : ∀ (f : ContMDiffMap I () G 𝕜 ), X f = Y f) :
X = Y
theorem LeftInvariantDerivation.coe_derivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) :
X = X
theorem LeftInvariantDerivation.left_invariant' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (X : ) :
() ( X) = X

Premature version of the lemma. Prefer using left_invariant instead.

theorem LeftInvariantDerivation.map_add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (f : ContMDiffMap I () G 𝕜 ) {f' : ContMDiffMap I () G 𝕜 } :
X (f + f') = X f + X f'
theorem LeftInvariantDerivation.map_zero {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) :
X 0 = 0
theorem LeftInvariantDerivation.map_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (f : ContMDiffMap I () G 𝕜 ) :
X (-f) = -X f
theorem LeftInvariantDerivation.map_sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (f : ContMDiffMap I () G 𝕜 ) {f' : ContMDiffMap I () G 𝕜 } :
X (f - f') = X f - X f'
theorem LeftInvariantDerivation.map_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] {r : 𝕜} (X : ) (f : ContMDiffMap I () G 𝕜 ) :
X (r f) = r X f
@[simp]
theorem LeftInvariantDerivation.leibniz {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (f : ContMDiffMap I () G 𝕜 ) {f' : ContMDiffMap I () G 𝕜 } :
X (f * f') = f X f' + f' X f
instance LeftInvariantDerivation.instZeroLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instZeroLeftInvariantDerivation = { zero := { toDerivation := 0, left_invariant'' := } }
instance LeftInvariantDerivation.instInhabitedLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instInhabitedLeftInvariantDerivation = { default := 0 }
instance LeftInvariantDerivation.instAddLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instAddLeftInvariantDerivation = { add := fun (X Y : ) => { toDerivation := X + Y, left_invariant'' := } }
instance LeftInvariantDerivation.instNegLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instNegLeftInvariantDerivation = { neg := fun (X : ) => { toDerivation := -X, left_invariant'' := } }
instance LeftInvariantDerivation.instSubLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instSubLeftInvariantDerivation = { sub := fun (X Y : ) => { toDerivation := X - Y, left_invariant'' := } }
@[simp]
theorem LeftInvariantDerivation.coe_add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (Y : ) :
(X + Y) = X + Y
@[simp]
theorem LeftInvariantDerivation.coe_zero {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
0 = 0
@[simp]
theorem LeftInvariantDerivation.coe_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) :
(-X) = -X
@[simp]
theorem LeftInvariantDerivation.coe_sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (Y : ) :
(X - Y) = X - Y
@[simp]
theorem LeftInvariantDerivation.lift_add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (Y : ) :
(X + Y) = X + Y
@[simp]
theorem LeftInvariantDerivation.lift_zero {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
0 = 0
instance LeftInvariantDerivation.hasNatScalar {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.hasNatScalar = { smul := fun (r : ) (X : ) => { toDerivation := r X, left_invariant'' := } }
instance LeftInvariantDerivation.hasIntScalar {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.hasIntScalar = { smul := fun (r : ) (X : ) => { toDerivation := r X, left_invariant'' := } }
instance LeftInvariantDerivation.instAddCommGroupLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
instance LeftInvariantDerivation.instSMulLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
SMul 𝕜 ()
Equations
• LeftInvariantDerivation.instSMulLeftInvariantDerivation = { smul := fun (r : 𝕜) (X : ) => { toDerivation := r X, left_invariant'' := } }
@[simp]
theorem LeftInvariantDerivation.coe_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (r : 𝕜) (X : ) :
(r X) = r X
@[simp]
theorem LeftInvariantDerivation.lift_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (k : 𝕜) :
(k X) = k X
@[simp]
theorem LeftInvariantDerivation.coeFnAddMonoidHom_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) (G : Type u_4) [] [] [] [] :
∀ (a : ) (a_1 : ContMDiffMap I () G 𝕜 ), = a a_1
def LeftInvariantDerivation.coeFnAddMonoidHom {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) (G : Type u_4) [] [] [] [] :
→+ ContMDiffMap I () G 𝕜 ContMDiffMap I () G 𝕜

The coercion to function is a monoid homomorphism.

Equations
• = { toZeroHom := { toFun := DFunLike.coe, map_zero' := }, map_add' := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
def LeftInvariantDerivation.evalAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) :

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

Equations
• = { toAddHom := { toFun := fun (X : ) => X, map_add' := }, map_smul' := }
Instances For
theorem LeftInvariantDerivation.evalAt_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (X : ) (f : ContMDiffMap I () G 𝕜 ) :
() f = (X f) g
@[simp]
theorem LeftInvariantDerivation.evalAt_coe {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (X : ) :
X =
theorem LeftInvariantDerivation.left_invariant {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (X : ) :
() () =
theorem LeftInvariantDerivation.evalAt_mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (h : G) (X : ) :
() X = () ()
theorem LeftInvariantDerivation.comp_L {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (g : G) (X : ) (f : ContMDiffMap I () G 𝕜 ) :
ContMDiffMap.comp (X f) () = X ()
instance LeftInvariantDerivation.instBracketLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instBracketLeftInvariantDerivation = { bracket := fun (X Y : ) => { toDerivation := X, Y, left_invariant'' := } }
@[simp]
theorem LeftInvariantDerivation.commutator_coe_derivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (Y : ) :
X, Y = X, Y
theorem LeftInvariantDerivation.commutator_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] (X : ) (Y : ) (f : ContMDiffMap I () G 𝕜 ) :
X, Y f = X (Y f) - Y (X f)
instance LeftInvariantDerivation.instLieRingLeftInvariantDerivation {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {G : Type u_4} [] [] [] [] :
Equations
• LeftInvariantDerivation.instLieRingLeftInvariantDerivation = LieRing.mk
Equations
• LeftInvariantDerivation.instLieAlgebraLeftInvariantDerivationToCommRingToEuclideanDomainToFieldToNormedFieldInstLieRingLeftInvariantDerivation =