Left invariant derivations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 left_invariant_derivation 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
left_invariant_derivation
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(G : Type u_4)
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Type (max u_1 u_4)
- to_derivation : derivation 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤)
- left_invariant'' : ∀ (g : G), ⇑(hfdifferential _) (⇑(derivation.eval_at 1) self.to_derivation) = ⇑(derivation.eval_at g) self.to_derivation
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 left_invariant_derivation
- left_invariant_derivation.has_sizeof_inst
- left_invariant_derivation.derivation.has_coe
- left_invariant_derivation.has_coe_to_fun
- left_invariant_derivation.has_zero
- left_invariant_derivation.inhabited
- left_invariant_derivation.has_add
- left_invariant_derivation.has_neg
- left_invariant_derivation.has_sub
- left_invariant_derivation.has_nat_scalar
- left_invariant_derivation.has_int_scalar
- left_invariant_derivation.add_comm_group
- left_invariant_derivation.has_smul
- left_invariant_derivation.module
- left_invariant_derivation.has_bracket
- left_invariant_derivation.lie_ring
- left_invariant_derivation.lie_algebra
@[protected, instance]
def
left_invariant_derivation.derivation.has_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
has_coe (left_invariant_derivation I G) (derivation 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤))
Equations
- left_invariant_derivation.derivation.has_coe = {coe := λ (X : left_invariant_derivation I G), X.to_derivation}
@[protected, instance]
def
left_invariant_derivation.has_coe_to_fun
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
has_coe_to_fun (left_invariant_derivation I G) (λ (_x : left_invariant_derivation I G), cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤ → cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤)
Equations
theorem
left_invariant_derivation.to_fun_eq_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
{X : left_invariant_derivation I G} :
theorem
left_invariant_derivation.coe_to_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
{X : left_invariant_derivation I G} :
@[simp]
theorem
left_invariant_derivation.to_derivation_eq_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
{X : left_invariant_derivation I G} :
X.to_derivation = ↑X
theorem
left_invariant_derivation.coe_injective
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
@[ext]
theorem
left_invariant_derivation.ext
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
{X Y : left_invariant_derivation I G}
(h : ∀ (f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤), ⇑X f = ⇑Y f) :
X = Y
theorem
left_invariant_derivation.coe_derivation
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G) :
theorem
left_invariant_derivation.coe_derivation_injective
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
theorem
left_invariant_derivation.left_invariant'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G)
(X : left_invariant_derivation I G) :
⇑(hfdifferential _) (⇑(derivation.eval_at 1) ↑X) = ⇑(derivation.eval_at g) ↑X
Premature version of the lemma. Prefer using left_invariant instead.
@[simp]
theorem
left_invariant_derivation.map_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤)
{f' : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤} :
@[simp]
theorem
left_invariant_derivation.map_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G) :
@[simp]
theorem
left_invariant_derivation.map_neg
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
@[simp]
theorem
left_invariant_derivation.map_sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤)
{f' : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤} :
@[simp]
theorem
left_invariant_derivation.map_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
{r : 𝕜}
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
@[simp]
theorem
left_invariant_derivation.leibniz
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤)
{f' : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤} :
@[protected, instance]
def
left_invariant_derivation.has_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_zero = {zero := {to_derivation := 0, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.inhabited
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
@[protected, instance]
def
left_invariant_derivation.has_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_add = {add := λ (X Y : left_invariant_derivation I G), {to_derivation := ↑X + ↑Y, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_neg
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_neg = {neg := λ (X : left_invariant_derivation I G), {to_derivation := -↑X, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_sub = {sub := λ (X Y : left_invariant_derivation I G), {to_derivation := ↑X - ↑Y, left_invariant'' := _}}
@[simp]
theorem
left_invariant_derivation.coe_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X Y : left_invariant_derivation I G) :
@[simp]
theorem
left_invariant_derivation.coe_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
@[simp]
theorem
left_invariant_derivation.coe_neg
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G) :
@[simp]
theorem
left_invariant_derivation.coe_sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X Y : left_invariant_derivation I G) :
@[simp, norm_cast]
theorem
left_invariant_derivation.lift_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X Y : left_invariant_derivation I G) :
@[simp, norm_cast]
theorem
left_invariant_derivation.lift_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
@[protected, instance]
def
left_invariant_derivation.has_nat_scalar
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_nat_scalar = {smul := λ (r : ℕ) (X : left_invariant_derivation I G), {to_derivation := r • ↑X, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.has_int_scalar
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_int_scalar = {smul := λ (r : ℤ) (X : left_invariant_derivation I G), {to_derivation := r • ↑X, left_invariant'' := _}}
@[protected, instance]
def
left_invariant_derivation.add_comm_group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.add_comm_group = function.injective.add_comm_group coe_fn left_invariant_derivation.coe_injective left_invariant_derivation.coe_zero left_invariant_derivation.coe_add left_invariant_derivation.coe_neg left_invariant_derivation.coe_sub left_invariant_derivation.add_comm_group._proof_2 left_invariant_derivation.add_comm_group._proof_3
@[protected, instance]
def
left_invariant_derivation.has_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
has_smul 𝕜 (left_invariant_derivation I G)
Equations
- left_invariant_derivation.has_smul = {smul := λ (r : 𝕜) (X : left_invariant_derivation I G), {to_derivation := r • ↑X, left_invariant'' := _}}
@[simp]
theorem
left_invariant_derivation.coe_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(r : 𝕜)
(X : left_invariant_derivation I G) :
@[simp]
theorem
left_invariant_derivation.lift_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(k : 𝕜) :
@[simp]
theorem
left_invariant_derivation.coe_fn_add_monoid_hom_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(G : Type u_4)
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X : left_invariant_derivation I G)
(ᾰ : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
def
left_invariant_derivation.coe_fn_add_monoid_hom
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(G : Type u_4)
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
left_invariant_derivation I G →+ cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤ → cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤
The coercion to function is a monoid homomorphism.
Equations
- left_invariant_derivation.coe_fn_add_monoid_hom I G = {to_fun := λ (X : left_invariant_derivation I G), X.to_derivation.to_linear_map.to_fun, map_zero' := _, map_add' := _}
@[protected, instance]
def
left_invariant_derivation.module
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
module 𝕜 (left_invariant_derivation I G)
def
left_invariant_derivation.eval_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G) :
Evaluation at a point for left invariant derivation. Same thing as for generic global
derivations (derivation.eval_at).
Equations
- left_invariant_derivation.eval_at g = {to_fun := λ (X : left_invariant_derivation I G), ⇑(derivation.eval_at g) ↑X, map_add' := _, map_smul' := _}
theorem
left_invariant_derivation.eval_at_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G)
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
@[simp]
theorem
left_invariant_derivation.eval_at_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G)
(X : left_invariant_derivation I G) :
⇑(derivation.eval_at g) ↑X = ⇑(left_invariant_derivation.eval_at g) X
theorem
left_invariant_derivation.left_invariant
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G)
(X : left_invariant_derivation I G) :
⇑(hfdifferential _) (⇑(left_invariant_derivation.eval_at 1) X) = ⇑(left_invariant_derivation.eval_at g) X
theorem
left_invariant_derivation.eval_at_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g h : G)
(X : left_invariant_derivation I G) :
⇑(left_invariant_derivation.eval_at (g * h)) X = ⇑(hfdifferential _) (⇑(left_invariant_derivation.eval_at h) X)
theorem
left_invariant_derivation.comp_L
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(g : G)
(X : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
(⇑X f).comp (smooth_left_mul I g) = ⇑X (f.comp (smooth_left_mul I g))
@[protected, instance]
def
left_invariant_derivation.has_bracket
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.has_bracket = {bracket := λ (X Y : left_invariant_derivation I G), {to_derivation := ⁅↑X, ↑Y⁆, left_invariant'' := _}}
@[simp]
theorem
left_invariant_derivation.commutator_coe_derivation
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X Y : left_invariant_derivation I G) :
theorem
left_invariant_derivation.commutator_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G]
(X Y : left_invariant_derivation I G)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) G 𝕜 ⊤) :
@[protected, instance]
def
left_invariant_derivation.lie_ring
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
Equations
- left_invariant_derivation.lie_ring = {to_add_comm_group := left_invariant_derivation.add_comm_group _inst_8, to_has_bracket := left_invariant_derivation.has_bracket _inst_8, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[protected, instance]
def
left_invariant_derivation.lie_algebra
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[topological_space G]
[charted_space H G]
[monoid G]
[has_smooth_mul I G] :
lie_algebra 𝕜 (left_invariant_derivation I G)
Equations
- left_invariant_derivation.lie_algebra = {to_module := left_invariant_derivation.module _inst_8, lie_smul := _}