mathlib documentation

geometry.manifold.algebra.left_invariant_derivation

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 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (G : Type u_4) [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I 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.

@[instance]
def left_invariant_derivation.derivation.has_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
has_coe (left_invariant_derivation I G) (derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
Equations
@[instance]
def left_invariant_derivation.has_coe_to_fun {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
theorem left_invariant_derivation.to_fun_eq_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] {X : left_invariant_derivation I G} :
theorem left_invariant_derivation.coe_to_linear_map {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] {X : left_invariant_derivation I G} :
@[simp]
theorem left_invariant_derivation.to_derivation_eq_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] {X : left_invariant_derivation I G} :
theorem left_invariant_derivation.coe_injective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
@[ext]
theorem left_invariant_derivation.ext {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] {X Y : left_invariant_derivation I G} (h : ∀ (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯), ⇑X f = ⇑Y f) :
X = Y
theorem left_invariant_derivation.coe_derivation {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) :
theorem left_invariant_derivation.coe_derivation_injective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
theorem left_invariant_derivation.left_invariant' {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g : G) (X : left_invariant_derivation I G) :

Premature version of the lemma. Prefer using left_invariant instead.

@[simp]
theorem left_invariant_derivation.map_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) {f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯} :
⇑X (f + f') = ⇑X f + ⇑X f'
@[simp]
theorem left_invariant_derivation.map_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) :
⇑X 0 = 0
@[simp]
theorem left_invariant_derivation.map_neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
⇑X (-f) = -⇑X f
@[simp]
theorem left_invariant_derivation.map_sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) {f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯} :
⇑X (f - f') = ⇑X f - ⇑X f'
@[simp]
theorem left_invariant_derivation.map_smul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] {r : 𝕜} (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
@[simp]
theorem left_invariant_derivation.leibniz {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) {f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯} :
⇑X (f * f') = f • ⇑X f' + f' • ⇑X f
@[instance]
def left_invariant_derivation.has_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[instance]
def left_invariant_derivation.inhabited {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[instance]
def left_invariant_derivation.has_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[instance]
def left_invariant_derivation.has_neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[instance]
def left_invariant_derivation.has_sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[simp]
theorem left_invariant_derivation.coe_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X Y : left_invariant_derivation I G) :
@[simp]
theorem left_invariant_derivation.coe_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
@[simp]
theorem left_invariant_derivation.coe_neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) :
@[simp]
theorem left_invariant_derivation.coe_sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X Y : left_invariant_derivation I G) :
@[simp]
theorem left_invariant_derivation.lift_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X Y : left_invariant_derivation I G) :
@[simp]
theorem left_invariant_derivation.lift_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
@[instance]
def left_invariant_derivation.has_scalar {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations
@[simp]
theorem left_invariant_derivation.coe_smul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (r : 𝕜) (X : left_invariant_derivation I G) :
@[simp]
theorem left_invariant_derivation.lift_smul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (k : 𝕜) :
@[simp]
theorem left_invariant_derivation.coe_fn_add_monoid_hom_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (G : Type u_4) [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X : left_invariant_derivation I G) (áž° : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
def left_invariant_derivation.coe_fn_add_monoid_hom {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (G : Type u_4) [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
left_invariant_derivation I G →+ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ → C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯

The coercion to function is a monoid homomorphism.

Equations
def left_invariant_derivation.eval_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g : G) (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
@[simp]
theorem left_invariant_derivation.eval_at_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g : G) (X : left_invariant_derivation I G) :
theorem left_invariant_derivation.left_invariant {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g : G) (X : left_invariant_derivation I G) :
theorem left_invariant_derivation.eval_at_mul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g h : G) (X : left_invariant_derivation I G) :
theorem left_invariant_derivation.comp_L {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (g : G) (X : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
(⇑X f).comp (𝑳 I g) = ⇑X (f.comp (𝑳 I g))
@[simp]
theorem left_invariant_derivation.commutator_coe_derivation {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X Y : left_invariant_derivation I G) :
theorem left_invariant_derivation.commutator_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (X Y : left_invariant_derivation I G) (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
@[instance]
def left_invariant_derivation.lie_algebra {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {G : Type u_4} [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] :
Equations