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.
Note that one can also define a Lie algebra on the space of left-invariant vector fields
(see instLieAlgebraGroupLieAlgebra). For finite-dimensional C^∞ real manifolds, the space of
derivations can be canonically identified with the tangent space, and we recover the same Lie
algebra structure (TODO: prove this). In other smoothness classes or on other
fields, this identification is not always true, though, so the derivations point of view does not
work in these settings. The left-invariant vector fields should
therefore be favored to construct a theory of Lie groups in suitable generality.
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]
[ContMDiffMul I (↑⊤) G]
extends Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) :
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
- 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
instance
LeftInvariantDerivation.instCoeDerivationContMDiffMapModelWithCornersSelfSomeENatTop
{𝕜 : 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]
[ContMDiffMul I (↑⊤) G]
:
Coe (LeftInvariantDerivation I G)
(Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤))
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]
[ContMDiffMul I (↑⊤) G]
:
instance
LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop
{𝕜 : 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]
[ContMDiffMul I (↑⊤) G]
:
FunLike (LeftInvariantDerivation I G) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
Equations
- LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop = { coe := fun (f : LeftInvariantDerivation I G) => ⇑↑f, coe_injective' := ⋯ }
instance
LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
{𝕜 : 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]
[ContMDiffMul I (↑⊤) G]
:
LinearMapClass (LeftInvariantDerivation I G) 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
(ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
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]
[ContMDiffMul I (↑⊤) G]
{X : LeftInvariantDerivation I G}
:
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]
[ContMDiffMul I (↑⊤) G]
:
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]
[ContMDiffMul I (↑⊤) G]
{X Y : LeftInvariantDerivation I G}
(h : ∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤), X f = Y f)
:
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]
[ContMDiffMul I (↑⊤) G]
{X Y : LeftInvariantDerivation I G}
:
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]
[ContMDiffMul I (↑⊤) G]
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul I (↑⊤) G]
(g : G)
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
:
Zero (LeftInvariantDerivation I G)
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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
(X 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]
[ContMDiffMul I (↑⊤) G]
:
@[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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
(X 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]
[ContMDiffMul I (↑⊤) G]
(X 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]
[ContMDiffMul I (↑⊤) G]
:
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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
:
Equations
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]
[ContMDiffMul 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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
(X : LeftInvariantDerivation I G)
(k : 𝕜)
:
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]
[ContMDiffMul 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
@[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]
[ContMDiffMul I (↑⊤) G]
(a✝ : LeftInvariantDerivation I G)
(a : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
:
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]
[ContMDiffMul I (↑⊤) G]
:
Module 𝕜 (LeftInvariantDerivation 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]
[ContMDiffMul I (↑⊤) G]
(g : 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]
[ContMDiffMul I (↑⊤) G]
(g : G)
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) 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]
[ContMDiffMul I (↑⊤) G]
(g : G)
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul I (↑⊤) G]
(g : G)
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul I (↑⊤) G]
(g h : G)
(X : LeftInvariantDerivation I G)
:
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]
[ContMDiffMul I (↑⊤) G]
(g : G)
(X : LeftInvariantDerivation I G)
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) 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]
[ContMDiffMul 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]
[ContMDiffMul I (↑⊤) G]
(X 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]
[ContMDiffMul I (↑⊤) G]
(X 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]
[ContMDiffMul I (↑⊤) G]
:
Equations
- One or more equations did not get rendered due to their size.
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]
[ContMDiffMul I (↑⊤) G]
:
LieAlgebra 𝕜 (LeftInvariantDerivation I G)
Equations
- LeftInvariantDerivation.instLieAlgebra = { toModule := LeftInvariantDerivation.instModule, lie_smul := ⋯ }