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 LeftInvariantDerivation 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.
- toFun : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤ → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤
- map_add' : ∀ (x y : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : 𝕜) (x : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id 𝕜) r • AddHom.toFun s.toAddHom x
- map_one_eq_zero' : ↑↑↑s 1 = 0
- leibniz' : ∀ (a b : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), ↑↑↑s (a * b) = a • ↑↑↑s b + b • ↑↑↑s a
- left_invariant'' : ∀ (g : G), ↑(hfdifferential (_ : ↑(smoothLeftMul I g) 1 = g)) (↑(Derivation.evalAt 1) ↑s) = ↑(Derivation.evalAt g) ↑s
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
Premature version of the lemma. Prefer using left_invariant
instead.
The coercion to function is a monoid homomorphism.
Instances For
Evaluation at a point for left invariant derivation. Same thing as for generic global
derivations (Derivation.evalAt
).