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)
- 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
instance
LeftInvariantDerivation.instCoeLeftInvariantDerivationDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTopToCommSemiringToSemifieldToFieldToCommSemiringCommRingToCommRingToEuclideanDomainFieldSmoothRingSmoothFunctionsAlgebraAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingHasSmoothAddSelfModule'Module
{𝕜 : 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 𝕜 ⊤))
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.instLinearMapClassLeftInvariantDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTopToSemiringToDivisionSemiringToSemifieldToFieldAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingHasSmoothAddSelfModule
{𝕜 : 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 𝕜 ⊤)
instance
LeftInvariantDerivation.instCoeFunLeftInvariantDerivationForAllContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNormedRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTop
{𝕜 : 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]
:
CoeFun (LeftInvariantDerivation I G) fun x =>
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]
[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 FunLike.coe
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 (_ : ↑(smoothLeftMul I g) 1 = g)) (↑(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.instZeroLeftInvariantDerivation
{𝕜 : 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)
instance
LeftInvariantDerivation.instInhabitedLeftInvariantDerivation
{𝕜 : 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]
:
instance
LeftInvariantDerivation.instAddLeftInvariantDerivation
{𝕜 : 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)
instance
LeftInvariantDerivation.instNegLeftInvariantDerivation
{𝕜 : 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)
instance
LeftInvariantDerivation.instSubLeftInvariantDerivation
{𝕜 : 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)
@[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)
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)
instance
LeftInvariantDerivation.instAddCommGroupLeftInvariantDerivation
{𝕜 : 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]
:
instance
LeftInvariantDerivation.instSMulLeftInvariantDerivation
{𝕜 : 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)
@[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.
Instances For
instance
LeftInvariantDerivation.instModuleLeftInvariantDerivationToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToAddCommMonoidInstAddCommGroupLeftInvariantDerivation
{𝕜 : 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)
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).
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 (_ : ↑(smoothLeftMul I g) 1 = g)) (↑(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 (_ : ↑(smoothLeftMul I g) h = g * h)) (↑(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 𝕜 ⊤)
:
ContMDiffMap.comp (↑X f) (smoothLeftMul I g) = ↑X (ContMDiffMap.comp f (smoothLeftMul I g))
instance
LeftInvariantDerivation.instBracketLeftInvariantDerivation
{𝕜 : 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)
@[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.instLieRingLeftInvariantDerivation
{𝕜 : 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]
:
instance
LeftInvariantDerivation.instLieAlgebraLeftInvariantDerivationToCommRingToEuclideanDomainToFieldToNormedFieldInstLieRingLeftInvariantDerivation
{𝕜 : 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)