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.
- 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
Equations
- left_invariant_derivation.derivation.has_coe = {coe := Ξ» (X : left_invariant_derivation I G), X.to_derivation}
Equations
- left_invariant_derivation.has_coe_to_fun = {coe := Ξ» (X : left_invariant_derivation I G), X.to_derivation.to_linear_map.to_fun}
Premature version of the lemma. Prefer using left_invariant
instead.
Equations
- left_invariant_derivation.has_zero = {zero := {to_derivation := 0, left_invariant'' := _}}
Equations
Equations
- left_invariant_derivation.has_add = {add := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := βX + βY, left_invariant'' := _}}
Equations
- left_invariant_derivation.has_neg = {neg := Ξ» (X : left_invariant_derivation I G), {to_derivation := -βX, left_invariant'' := _}}
Equations
- left_invariant_derivation.has_sub = {sub := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := βX - βY, left_invariant'' := _}}
Equations
- left_invariant_derivation.has_nat_scalar = {smul := Ξ» (r : β) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
Equations
- left_invariant_derivation.has_int_scalar = {smul := Ξ» (r : β€) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
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
Equations
- left_invariant_derivation.has_smul = {smul := Ξ» (r : π) (X : left_invariant_derivation I G), {to_derivation := r β’ βX, left_invariant'' := _}}
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' := _}
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' := _}
Equations
- left_invariant_derivation.has_bracket = {bracket := Ξ» (X Y : left_invariant_derivation I G), {to_derivation := β βX, βYβ, left_invariant'' := _}}
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 := _}
Equations
- left_invariant_derivation.lie_algebra = {to_module := left_invariant_derivation.module _inst_8, lie_smul := _}