English
If D is a nilpotent derivation on an algebra B (with suitable module structure), then exp(D) respects multiplication, i.e., exp(D)(x y) = exp(D)(x) exp(D)(y) for x,y ∈ B.
Русский
Если $D$ — нильпотентная производная на алгебре $B$, то экспонента сохраняет умножение: $\exp(D)(xy) = \exp(D)(x) \exp(D)(y)$.
LaTeX
$$$\exp(D)(xy) = \exp(D)(x) \exp(D)(y)$$$
Lean4
theorem exp_mul_of_derivation (R B : Type*) [CommRing R] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B]
[IsScalarTower R B B] [Module ℚ B] (D : B →ₗ[R] B) (h_der : ∀ x y, D (x * y) = x * D y + (D x) * y)
(h_nil : IsNilpotent D) (x y : B) : exp D (x * y) = (exp D x) * (exp D y) :=
by
let DL : Module.End R (B ⊗[R] B) := D.lTensor B
let DR : Module.End R (B ⊗[R] B) := D.rTensor B
have h_nilL : IsNilpotent DL := h_nil.map <| lTensorAlgHom R B B
have h_nilR : IsNilpotent DR := h_nil.map <| rTensorAlgHom R B B
have h_comm : Commute DL DR := by ext; simp [DL, DR]
set m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B with hm
have h₁ : exp D (x * y) = m (exp (DL + DR) (x ⊗ₜ[R] y)) :=
by
suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)
apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil
ext
simp [DL, DR, hm, h_der]
have h₂ : exp DL = (exp D).lTensor B := (h_nil.map_exp (lTensorAlgHom R B B)).symm
have h₃ : exp DR = (exp D).rTensor B := (h_nil.map_exp (rTensorAlgHom R B B)).symm
simp [h₁, exp_add_of_commute h_comm h_nilL h_nilR, h₂, h₃, hm]
