# mathlib3documentation

geometry.manifold.algebra.left_invariant_derivation

# Left invariant derivations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 left_invariant_derivation 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 left_invariant_derivation {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [monoid G] [ G] :
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 left_invariant_derivation
@[protected, instance]
def left_invariant_derivation.derivation.has_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
G 𝕜 ) G 𝕜 ))
Equations
@[protected, instance]
def left_invariant_derivation.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
(λ (_x : , G 𝕜 G 𝕜 )
Equations
theorem left_invariant_derivation.to_fun_eq_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] {X : G} :
theorem left_invariant_derivation.coe_to_linear_map {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] {X : G} :
@[simp]
theorem left_invariant_derivation.to_derivation_eq_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] {X : G} :
theorem left_invariant_derivation.coe_injective {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
@[ext]
theorem left_invariant_derivation.ext {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] {X Y : G} (h : (f : G 𝕜 ), X f = Y f) :
X = Y
theorem left_invariant_derivation.coe_derivation {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) :
theorem left_invariant_derivation.coe_derivation_injective {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
theorem left_invariant_derivation.left_invariant' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) (X : G) :

Premature version of the lemma. Prefer using left_invariant instead.

@[simp]
theorem left_invariant_derivation.map_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) (f : G 𝕜 ) {f' : G 𝕜 } :
X (f + f') = X f + X f'
@[simp]
theorem left_invariant_derivation.map_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) :
X 0 = 0
@[simp]
theorem left_invariant_derivation.map_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) (f : G 𝕜 ) :
X (-f) = -X f
@[simp]
theorem left_invariant_derivation.map_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) (f : G 𝕜 ) {f' : G 𝕜 } :
X (f - f') = X f - X f'
@[simp]
theorem left_invariant_derivation.map_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] {r : 𝕜} (X : G) (f : G 𝕜 ) :
X (r f) = r X f
@[simp]
theorem left_invariant_derivation.leibniz {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) (f : G 𝕜 ) {f' : G 𝕜 } :
X (f * f') = f X f' + f' X f
@[protected, instance]
def left_invariant_derivation.has_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.inhabited {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.has_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.has_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.has_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[simp]
theorem left_invariant_derivation.coe_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X Y : G) :
(X + Y) = X + Y
@[simp]
theorem left_invariant_derivation.coe_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
0 = 0
@[simp]
theorem left_invariant_derivation.coe_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) :
@[simp]
theorem left_invariant_derivation.coe_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X Y : G) :
(X - Y) = X - Y
@[simp, norm_cast]
theorem left_invariant_derivation.lift_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X Y : G) :
(X + Y) = X + Y
@[simp, norm_cast]
theorem left_invariant_derivation.lift_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
0 = 0
@[protected, instance]
def left_invariant_derivation.has_nat_scalar {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.has_int_scalar {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.add_comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.has_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[simp]
theorem left_invariant_derivation.coe_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (r : 𝕜) (X : G) :
(r X) = r X
@[simp]
theorem left_invariant_derivation.lift_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X : G) (k : 𝕜) :
(k X) = k X
@[simp]
theorem left_invariant_derivation.coe_fn_add_monoid_hom_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [monoid G] [ G] (X : G) (ᾰ : G 𝕜 ) :
def left_invariant_derivation.coe_fn_add_monoid_hom {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [monoid G] [ G] :
→+ G 𝕜 G 𝕜

The coercion to function is a monoid homomorphism.

Equations
@[protected, instance]
def left_invariant_derivation.module {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
def left_invariant_derivation.eval_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) :

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

Equations
theorem left_invariant_derivation.eval_at_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) (X : G) (f : G 𝕜 ) :
f = (X f) g
@[simp]
theorem left_invariant_derivation.eval_at_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) (X : G) :
theorem left_invariant_derivation.left_invariant {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) (X : G) :
theorem left_invariant_derivation.eval_at_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g h : G) (X : G) :
X =
theorem left_invariant_derivation.comp_L {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (g : G) (X : G) (f : G 𝕜 ) :
(X f).comp g) = X (f.comp g))
@[protected, instance]
def left_invariant_derivation.has_bracket {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[simp]
theorem left_invariant_derivation.commutator_coe_derivation {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X Y : G) :
theorem left_invariant_derivation.commutator_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] (X Y : G) (f : G 𝕜 ) :
X, Y f = X (Y f) - Y (X f)
@[protected, instance]
def left_invariant_derivation.lie_ring {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations
@[protected, instance]
def left_invariant_derivation.lie_algebra {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {G : Type u_4} [ G] [monoid G] [ G] :
Equations