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