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.
structure
LeftInvariantDerivation
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(G : Type u_4)
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
extends
Derivation
:
Type (max u_1 u_4)
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).toFun (x + y) = (↑↑self).toFun x + (↑↑self).toFun y
- map_smul' : ∀ (m : 𝕜) (x : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), (↑↑self).toFun (m • x) = (RingHom.id 𝕜) m • (↑↑self).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 ⋯) ((Derivation.evalAt 1) ↑self) = (Derivation.evalAt g) ↑self
Instances For
theorem
LeftInvariantDerivation.left_invariant''
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(self : LeftInvariantDerivation I G)
(g : G)
:
(hfdifferential ⋯) ((Derivation.evalAt 1) ↑self) = (Derivation.evalAt g) ↑self
instance
LeftInvariantDerivation.instCoeDerivationContMDiffMapModelWithCornersSelfTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Coe (LeftInvariantDerivation I G)
(Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤))
Equations
- LeftInvariantDerivation.instCoeDerivationContMDiffMapModelWithCornersSelfTopENat = { coe := LeftInvariantDerivation.toDerivation }
theorem
LeftInvariantDerivation.toDerivation_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Function.Injective LeftInvariantDerivation.toDerivation
instance
LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
FunLike (LeftInvariantDerivation I G) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
Equations
- LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfTopENat = { coe := fun (f : LeftInvariantDerivation I G) => ⇑↑f, coe_injective' := ⋯ }
instance
LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
LinearMapClass (LeftInvariantDerivation I G) 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
Equations
- ⋯ = ⋯
theorem
LeftInvariantDerivation.toFun_eq_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
{X : LeftInvariantDerivation I G}
:
(↑↑X).toFun = ⇑X
theorem
LeftInvariantDerivation.coe_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Function.Injective DFunLike.coe
theorem
LeftInvariantDerivation.ext_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
{X : LeftInvariantDerivation I G}
{Y : LeftInvariantDerivation I G}
:
X = Y ↔ ∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), X f = Y f
theorem
LeftInvariantDerivation.ext
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
{X : LeftInvariantDerivation I G}
{Y : LeftInvariantDerivation I G}
(h : ∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), X f = Y f)
:
X = Y
theorem
LeftInvariantDerivation.coe_derivation
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
:
⇑↑X = ⇑X
theorem
LeftInvariantDerivation.left_invariant'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(X : LeftInvariantDerivation I G)
:
(hfdifferential ⋯) ((Derivation.evalAt 1) ↑X) = (Derivation.evalAt g) ↑X
Premature version of the lemma. Prefer using left_invariant instead.
theorem
LeftInvariantDerivation.map_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
{f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤}
:
theorem
LeftInvariantDerivation.map_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
:
X 0 = 0
theorem
LeftInvariantDerivation.map_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
:
theorem
LeftInvariantDerivation.map_sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
{f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤}
:
theorem
LeftInvariantDerivation.map_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
{r : 𝕜}
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
:
@[simp]
theorem
LeftInvariantDerivation.leibniz
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
{f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤}
:
instance
LeftInvariantDerivation.instZero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Zero (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instZero = { zero := { toDerivation := 0, left_invariant'' := ⋯ } }
instance
LeftInvariantDerivation.instInhabited
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Equations
- LeftInvariantDerivation.instInhabited = { default := 0 }
instance
LeftInvariantDerivation.instAdd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Add (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instAdd = { add := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := ↑X + ↑Y, left_invariant'' := ⋯ } }
instance
LeftInvariantDerivation.instNeg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Neg (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instNeg = { neg := fun (X : LeftInvariantDerivation I G) => { toDerivation := -↑X, left_invariant'' := ⋯ } }
instance
LeftInvariantDerivation.instSub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Sub (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instSub = { sub := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := ↑X - ↑Y, left_invariant'' := ⋯ } }
@[simp]
theorem
LeftInvariantDerivation.coe_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(Y : LeftInvariantDerivation I G)
:
@[simp]
theorem
LeftInvariantDerivation.coe_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
⇑0 = 0
@[simp]
theorem
LeftInvariantDerivation.coe_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
:
@[simp]
theorem
LeftInvariantDerivation.coe_sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(Y : LeftInvariantDerivation I G)
:
@[simp]
theorem
LeftInvariantDerivation.lift_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(Y : LeftInvariantDerivation I G)
:
@[simp]
theorem
LeftInvariantDerivation.lift_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
↑0 = 0
instance
LeftInvariantDerivation.hasNatScalar
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
SMul ℕ (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.hasNatScalar = { smul := fun (r : ℕ) (X : LeftInvariantDerivation I G) => { toDerivation := r • ↑X, left_invariant'' := ⋯ } }
instance
LeftInvariantDerivation.hasIntScalar
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
SMul ℤ (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.hasIntScalar = { smul := fun (r : ℤ) (X : LeftInvariantDerivation I G) => { toDerivation := r • ↑X, left_invariant'' := ⋯ } }
instance
LeftInvariantDerivation.instAddCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Equations
- LeftInvariantDerivation.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
LeftInvariantDerivation.instSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
SMul 𝕜 (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instSMul = { smul := fun (r : 𝕜) (X : LeftInvariantDerivation I G) => { toDerivation := r • ↑X, left_invariant'' := ⋯ } }
@[simp]
theorem
LeftInvariantDerivation.coe_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(r : 𝕜)
(X : LeftInvariantDerivation I G)
:
@[simp]
theorem
LeftInvariantDerivation.lift_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(k : 𝕜)
:
@[simp]
theorem
LeftInvariantDerivation.coeFnAddMonoidHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(G : Type u_4)
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
∀ (a : LeftInvariantDerivation I G) (a_1 : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤),
(LeftInvariantDerivation.coeFnAddMonoidHom I G) a a_1 = a a_1
def
LeftInvariantDerivation.coeFnAddMonoidHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(G : Type u_4)
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
LeftInvariantDerivation I G →+ ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤ → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤
The coercion to function is a monoid homomorphism.
Equations
- LeftInvariantDerivation.coeFnAddMonoidHom I G = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
instance
LeftInvariantDerivation.instModule
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Module 𝕜 (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instModule = Function.Injective.module 𝕜 (LeftInvariantDerivation.coeFnAddMonoidHom I G) ⋯ ⋯
def
LeftInvariantDerivation.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
:
LeftInvariantDerivation I G →ₗ[𝕜] PointDerivation I g
Evaluation at a point for left invariant derivation. Same thing as for generic global
derivations (Derivation.evalAt).
Equations
- LeftInvariantDerivation.evalAt g = { toFun := fun (X : LeftInvariantDerivation I G) => (Derivation.evalAt g) ↑X, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
LeftInvariantDerivation.evalAt_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
:
((LeftInvariantDerivation.evalAt g) X) f = (X f) g
@[simp]
theorem
LeftInvariantDerivation.evalAt_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(X : LeftInvariantDerivation I G)
:
(Derivation.evalAt g) ↑X = (LeftInvariantDerivation.evalAt g) X
theorem
LeftInvariantDerivation.left_invariant
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(X : LeftInvariantDerivation I G)
:
(hfdifferential ⋯) ((LeftInvariantDerivation.evalAt 1) X) = (LeftInvariantDerivation.evalAt g) X
theorem
LeftInvariantDerivation.evalAt_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(h : G)
(X : LeftInvariantDerivation I G)
:
(LeftInvariantDerivation.evalAt (g * h)) X = (hfdifferential ⋯) ((LeftInvariantDerivation.evalAt h) X)
theorem
LeftInvariantDerivation.comp_L
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(g : G)
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
:
(X f).comp (smoothLeftMul I g) = X (f.comp (smoothLeftMul I g))
instance
LeftInvariantDerivation.instBracket
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Bracket (LeftInvariantDerivation I G) (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instBracket = { bracket := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := ⁅↑X, ↑Y⁆, left_invariant'' := ⋯ } }
@[simp]
theorem
LeftInvariantDerivation.commutator_coe_derivation
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(Y : LeftInvariantDerivation I G)
:
theorem
LeftInvariantDerivation.commutator_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(X : LeftInvariantDerivation I G)
(Y : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤)
:
instance
LeftInvariantDerivation.instLieRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
Equations
- LeftInvariantDerivation.instLieRing = LieRing.mk ⋯ ⋯ ⋯ ⋯
instance
LeftInvariantDerivation.instLieAlgebra
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
:
LieAlgebra 𝕜 (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instLieAlgebra = LieAlgebra.mk ⋯