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)
- to_derivation : derivation π (cont_mdiff_map I (model_with_corners_self π π) G π β€) (cont_mdiff_map I (model_with_corners_self π π) G π β€)
- left_invariant'' : β (g : G), β(hfdifferential _) (β(derivation.eval_at 1) self.to_derivation) = β(derivation.eval_at g) self.to_derivation
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
- left_invariant_derivation.has_sizeof_inst
- left_invariant_derivation.derivation.has_coe
- left_invariant_derivation.has_coe_to_fun
- left_invariant_derivation.has_zero
- left_invariant_derivation.inhabited
- left_invariant_derivation.has_add
- left_invariant_derivation.has_neg
- left_invariant_derivation.has_sub
- left_invariant_derivation.has_nat_scalar
- left_invariant_derivation.has_int_scalar
- left_invariant_derivation.add_comm_group
- left_invariant_derivation.has_smul
- left_invariant_derivation.module
- left_invariant_derivation.has_bracket
- left_invariant_derivation.lie_ring
- left_invariant_derivation.lie_algebra
@[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
- left_invariant_derivation.derivation.has_coe = {coe := Ξ» (X : left_invariant_derivation I G), X.to_derivation}
@[protected, instance]
def
left_invariant_derivation.has_coe_to_fun
{π : 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_to_fun (left_invariant_derivation I G) (Ξ» (_x : left_invariant_derivation I G), cont_mdiff_map I (model_with_corners_self π π) G π β€ β cont_mdiff_map I (model_with_corners_self π π) G π β€)
Equations
- left_invariant_derivation.has_coe_to_fun = {coe := Ξ» (X : left_invariant_derivation I G), X.to_derivation.to_linear_map.to_fun}
theorem
left_invariant_derivation.to_fun_eq_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]
{X : left_invariant_derivation I G} :
theorem
left_invariant_derivation.coe_to_linear_map
{π : 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.to_derivation_eq_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]
{X : left_invariant_derivation I G} :
X.to_derivation = βX
theorem
left_invariant_derivation.coe_injective
{π : 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] :
@[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
theorem
left_invariant_derivation.coe_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]
(X : left_invariant_derivation I G) :
theorem
left_invariant_derivation.coe_derivation_injective
{π : 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] :
theorem
left_invariant_derivation.left_invariant'
{π : 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) :
β(hfdifferential _) (β(derivation.eval_at 1) βX) = β(derivation.eval_at g) βX
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 π β€} :
@[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) :
@[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 π β€) :
@[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 π β€} :
@[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 π β€} :
@[protected, instance]
def
left_invariant_derivation.has_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] :
Equations
- left_invariant_derivation.has_zero = {zero := {to_derivation := 0, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.inhabited
{π : 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
@[protected, instance]
def
left_invariant_derivation.has_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] :
Equations
- left_invariant_derivation.has_add = {add := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := βX + βY, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_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] :
Equations
- left_invariant_derivation.has_neg = {neg := Ξ» (X : left_invariant_derivation I G), {to_derivation := -βX, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_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] :
Equations
- left_invariant_derivation.has_sub = {sub := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := βX - βY, left_invariant'' := _}}
@[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_nat_scalar
{π : 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
- left_invariant_derivation.has_nat_scalar = {smul := Ξ» (r : β) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_int_scalar
{π : 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
- left_invariant_derivation.has_int_scalar = {smul := Ξ» (r : β€) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.add_comm_group
{π : 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
- left_invariant_derivation.add_comm_group = function.injective.add_comm_group coe_fn left_invariant_derivation.coe_injective left_invariant_derivation.coe_zero left_invariant_derivation.coe_add left_invariant_derivation.coe_neg left_invariant_derivation.coe_sub left_invariant_derivation.add_comm_group._proof_2 left_invariant_derivation.add_comm_group._proof_3
@[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] :
has_smul π (left_invariant_derivation I G)
Equations
- left_invariant_derivation.has_smul = {smul := Ξ» (r : π) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
@[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 : π) :
@[simp]
theorem
left_invariant_derivation.coe_fn_add_monoid_hom_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 : left_invariant_derivation I G)
(αΎ° : cont_mdiff_map I (model_with_corners_self π π) G π β€) :
β(left_invariant_derivation.coe_fn_add_monoid_hom I G) X αΎ° = X.to_derivation.to_linear_map.to_fun αΎ°
def
left_invariant_derivation.coe_fn_add_monoid_hom
{π : 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] :
left_invariant_derivation I G β+ cont_mdiff_map I (model_with_corners_self π π) G π β€ β cont_mdiff_map I (model_with_corners_self π π) G π β€
The coercion to function is a monoid homomorphism.
Equations
- left_invariant_derivation.coe_fn_add_monoid_hom I G = {to_fun := Ξ» (X : left_invariant_derivation I G), X.to_derivation.to_linear_map.to_fun, map_zero' := _, map_add' := _}
@[protected, instance]
def
left_invariant_derivation.module
{π : 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] :
module π (left_invariant_derivation I G)
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) :
left_invariant_derivation I G ββ[π] point_derivation I g
Evaluation at a point for left invariant derivation. Same thing as for generic global
derivations (derivation.eval_at).
Equations
- left_invariant_derivation.eval_at g = {to_fun := Ξ» (X : left_invariant_derivation I G), β(derivation.eval_at g) βX, map_add' := _, map_smul' := _}
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 π β€) :
@[simp]
theorem
left_invariant_derivation.eval_at_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]
(g : G)
(X : left_invariant_derivation I G) :
theorem
left_invariant_derivation.left_invariant
{π : 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) :
theorem
left_invariant_derivation.eval_at_mul
{π : 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 h : G)
(X : left_invariant_derivation I G) :
β(left_invariant_derivation.eval_at (g * h)) X = β(hfdifferential _) (β(left_invariant_derivation.eval_at h) X)
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 π β€) :
(βX f).comp (smooth_left_mul I g) = βX (f.comp (smooth_left_mul I g))
@[protected, instance]
def
left_invariant_derivation.has_bracket
{π : 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
- left_invariant_derivation.has_bracket = {bracket := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := β βX, βYβ, left_invariant'' := _}}
@[simp]
theorem
left_invariant_derivation.commutator_coe_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]
(X Y : left_invariant_derivation I 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 π β€) :
@[protected, instance]
def
left_invariant_derivation.lie_ring
{π : 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
- left_invariant_derivation.lie_ring = {to_add_comm_group := left_invariant_derivation.add_comm_group _inst_8, to_has_bracket := left_invariant_derivation.has_bracket _inst_8, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[protected, instance]
def
left_invariant_derivation.lie_algebra
{π : 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] :
lie_algebra π (left_invariant_derivation I G)
Equations
- left_invariant_derivation.lie_algebra = {to_module := left_invariant_derivation.module _inst_8, lie_smul := _}