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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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.

Instances for left_invariant_derivation
@[protected, instance]
def left_invariant_derivation.derivation.has_coe {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 π•œ (cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) (cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀))
Equations
@[ext]
theorem left_invariant_derivation.ext {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀), ⇑X f = ⇑Y f) :
X = Y

Premature version of the lemma. Prefer using left_invariant instead.

@[simp]
theorem left_invariant_derivation.map_add {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) {f' : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀} :
⇑X (f + f') = ⇑X f + ⇑X f'
@[simp]
theorem left_invariant_derivation.map_zero {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) :
⇑X (-f) = -⇑X f
@[simp]
theorem left_invariant_derivation.map_sub {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) {f' : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀} :
⇑X (f - f') = ⇑X f - ⇑X f'
@[simp]
theorem left_invariant_derivation.map_smul {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) :
@[simp]
theorem left_invariant_derivation.leibniz {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) {f' : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀} :
⇑X (f * f') = f β€’ ⇑X f' + f' β€’ ⇑X f
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem left_invariant_derivation.coe_add {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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, norm_cast]
theorem left_invariant_derivation.lift_add {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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, norm_cast]
theorem left_invariant_derivation.lift_zero {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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] :
@[protected, instance]
def left_invariant_derivation.has_smul {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : π•œ) :

The coercion to function is a monoid homomorphism.

Equations
def left_invariant_derivation.eval_at {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) :
theorem left_invariant_derivation.comp_L {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) :
theorem left_invariant_derivation.commutator_apply {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_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 : cont_mdiff_map I (model_with_corners_self π•œ π•œ) G π•œ ⊀) :