English
The map g ↦ mulInvariantVectorField v g is ContMDiff for minSmoothness 2.
Русский
Карта g ↦ mulInvariantVectorField v g гладка в смысле ContMDiff при минимальной гладкости 2.
LaTeX
$$ContMDiff I I (tangent) (minSmoothness 𝕜 2) (fun g => mulInvariantVectorField v g)$$
Lean4
@[to_additive]
theorem contMDiff_mulInvariantVectorField (v : GroupLieAlgebra I G) :
ContMDiff I I.tangent (minSmoothness 𝕜 2) (fun (g : G) ↦ (mulInvariantVectorField v g : TangentBundle I G)) := by
/- We will write the desired map as a composition of obviously smooth maps.
The derivative of the product `P : (g, h) ↦ g * h` is given by
`DP (g, h) ⬝ (u, v) = DL_g v + DR_h u`, where `L_g` and `R_h` are respectively left and right
multiplication by `g` and `h`. As `P` is smooth, so is `DP`.
Consider the map `F₁ : M → T (M × M)` mapping `g` to `(0, v) ∈ T_(g, e) (M × M)`. Then the
composition of `DP` with `F₁` maps `g` to `DL_g v ∈ T_g M`, thanks to the above formula. This
is the desired invariant vector field. Since both `DP` and `F₁` are smooth, their composition is
smooth as desired.
There is a small abuse of notation in the above argument, where we have identified `T (M × M)`
and `TM × TM`. In the formal proof, we need to introduce this identification, called `F₂` below,
which is also already known to be smooth. -/
have M : 1 ≤ minSmoothness 𝕜 3 := le_trans (by simp) le_minSmoothness
have A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3 :=
by
rw [← minSmoothness_add]
norm_num
let fg : G → TangentBundle I G := fun g ↦ TotalSpace.mk' E g 0
have sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg := contMDiff_zeroSection _ _
let fv : G → TangentBundle I G := fun _ ↦ TotalSpace.mk' E 1 v
have sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv := contMDiff_const
let F₁ : G → (TangentBundle I G × TangentBundle I G) := fun g ↦ (fg g, fv g)
have S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁ := ContMDiff.prodMk sfg sfv
let F₂ : (TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G) :=
(equivTangentBundleProd I G I G).symm
have S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂ :=
contMDiff_equivTangentBundleProd_symm
let F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I (fun (p : G × G) ↦ p.1 * p.2)
have S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃ :=
by
apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl
rw [A]
exact contMDiff_mul I (minSmoothness 𝕜 3)
let S := (S₃.comp S₂).comp S₁
convert S with g
· simp [F₁, F₂, F₃, fg, fv]
· simp only [comp_apply, tangentMap, F₃, F₂, F₁, fg, fv]
rw [mfderiv_prod_eq_add_apply ((contMDiff_mul I (minSmoothness 𝕜 3)).mdifferentiableAt M)]
simp [mulInvariantVectorField]
