mathlib3 documentation

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.

@[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]
@[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 𝕜 ) :
X (r f) = r X f
@[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
@[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) :
(X + Y) = X + Y
@[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] :
0 = 0
@[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) :
(X - Y) = X - Y
@[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) :
(X + Y) = X + Y
@[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] :
0 = 0
@[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) :
(r X) = r X
@[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 : 𝕜) :
(k X) = k X

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

Equations
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 𝕜 ) :