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' : ∀ (r : 𝕜) (x : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ⊤), self.toFun (r • x) = (RingHom.id 𝕜) r • 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
instance
LeftInvariantDerivation.instCoeLeftInvariantDerivationDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTopToCommSemiringToSemifieldToFieldToCommSemiringCommRingToCommRingToEuclideanDomainFieldSmoothRingAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingHasSmoothAddSelfSmoothFunctionsAlgebraModule'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 𝕜 ⊤))
Equations
- One or more equations did not get rendered due to their size.
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.instFunLikeLeftInvariantDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTop
{𝕜 : 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
- One or more equations did not get rendered due to their size.
instance
LeftInvariantDerivation.instLinearMapClassLeftInvariantDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTopToSemiringToDivisionSemiringToSemifieldToFieldAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingHasSmoothAddSelfModuleInstFunLikeLeftInvariantDerivationContMDiffMapToNormedAddCommGroupToNonUnitalNormedRingToNonUnitalNormedCommRingToNormedCommRingToNormedFieldToNormedSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingChartedSpaceSelfTopENatInstENatTop
{𝕜 : 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
{𝕜 : 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.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)
Equations
- LeftInvariantDerivation.instZeroLeftInvariantDerivation = { zero := { toDerivation := 0, left_invariant'' := ⋯ } }
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]
:
Equations
- LeftInvariantDerivation.instInhabitedLeftInvariantDerivation = { default := 0 }
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)
Equations
- LeftInvariantDerivation.instAddLeftInvariantDerivation = { add := fun (X Y : LeftInvariantDerivation I G) => { toDerivation := ↑X + ↑Y, left_invariant'' := ⋯ } }
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)
Equations
- LeftInvariantDerivation.instNegLeftInvariantDerivation = { neg := fun (X : LeftInvariantDerivation I G) => { toDerivation := -↑X, left_invariant'' := ⋯ } }
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)
Equations
- LeftInvariantDerivation.instSubLeftInvariantDerivation = { 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.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]
:
Equations
- LeftInvariantDerivation.instAddCommGroupLeftInvariantDerivation = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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)
Equations
- LeftInvariantDerivation.instSMulLeftInvariantDerivation = { 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 = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }
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)
Equations
- One or more equations did not get rendered due to their size.
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 = { toAddHom := { 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 𝕜 ⊤)
:
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)
Equations
- LeftInvariantDerivation.instBracketLeftInvariantDerivation = { 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.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]
:
Equations
- LeftInvariantDerivation.instLieRingLeftInvariantDerivation = LieRing.mk ⋯ ⋯ ⋯ ⋯
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)
Equations
- LeftInvariantDerivation.instLieAlgebraLeftInvariantDerivationToCommRingToEuclideanDomainToFieldToNormedFieldInstLieRingLeftInvariantDerivation = LieAlgebra.mk ⋯