English
The invariant vector field map at identity intertwines with mpullback along left-multiplication, giving equality with mpullback of mulInvariantVectorField v.
Русский
Инвариантное векторное поле взаимно переставляется с mpullback вдоль левого умножения, удовлетворяя равенство.
LaTeX
$$$mulInvariantVectorField \\,(V 1) g = mpullback I I (g^{-1} * \\cdot) V g$$$
Lean4
/-- Invariant vector fields are invariant under pullbacks. -/
@[to_additive /-- Invariant vector fields are invariant under pullbacks. -/
]
theorem mpullback_mulInvariantVectorField (g : G) (v : GroupLieAlgebra I G) :
mpullback I I (g * ·) (mulInvariantVectorField v) = mulInvariantVectorField v :=
by
have M : 1 ≤ minSmoothness 𝕜 3 := le_trans (by simp) le_minSmoothness
ext h
simp only [mpullback, inverse_mfderiv_mul_left, mulInvariantVectorField]
have D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ (fun x ↦ g * h * x) := by ext x; simp only [comp_apply]; group
rw [D, mfderiv_comp (I' := I)]
· congr 2
simp
· exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M
· exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M
