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 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
- left_invariant'' : ∀ (g : G), ⇑(𝒅ₕ _) (⇑(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
Premature version of the lemma. Prefer using
The coercion to function is a monoid homomorphism.
Evaluation at a point for left invariant derivation. Same thing as for generic global