instBracket — Mathlib

English

There is a canonical module structure over 𝕜 on LeftInvariantDerivation(I,G).

Русский

Существует каноническая структура модуля над 𝕜 на LeftInvariantDerivation(I,G).

LaTeX

$$$ \mathrm{LeftInvariantDerivation}(I,G) \text{ is a } \mathbb{K}\text{-module}$.$$

Lean4

instance : Bracket (LeftInvariantDerivation I G) (LeftInvariantDerivation I G) where
  bracket X
    Y :=
    ⟨⁅(X : Derivation 𝕜 C^∞⟮I, G; 𝕜⟯ C^∞⟮I, G; 𝕜⟯), Y⁆, fun g =>
      by
      ext f
      have hX := Derivation.congr_fun (left_invariant' g X) (Y f)
      have hY := Derivation.congr_fun (left_invariant' g Y) (X f)
      rw [hfdifferential_apply, fdifferential_apply, Derivation.evalAt_apply] at hX hY ⊢
      rw [comp_L] at hX hY
      rw [Derivation.commutator_apply, ContMDiffMap.coe_sub, Pi.sub_apply, coe_derivation]
      rw [coe_derivation] at hX hY ⊢
      rw [hX, hY]
      rfl⟩

Похожие утверждения