English
Let fM and fN be nilpotent endomorphisms of modules M and N, and let g: M → L N be a linear map with fN ∘ g = g ∘ fM. Then exp(fN) ∘ g = g ∘ exp(fM).
Русский
Пусть $f_M$ и $f_N$ — нильпотентные эндоморфизмы модулей $M$ и $N$, и пусть $g: M \to N$ линейно, удовлетворяющее $f_N\circ g = g\circ f_M$. Тогда экспоненты удовлетворяют $\exp(f_N)\circ g = g\circ \exp(f_M)$.
LaTeX
$$$\exp(f_N) \circ g = g \circ \exp(f_M)$$$
Lean4
theorem commute_exp_left_of_commute {fM : Module.End R M} {fN : Module.End R N} {g : M →ₗ[R] N} (hfM : IsNilpotent fM)
(hfN : IsNilpotent fN) (h : fN ∘ₗ g = g ∘ₗ fM) : exp fN ∘ₗ g = g ∘ₗ exp fM :=
by
ext m
obtain ⟨k, hfM⟩ := hfM
obtain ⟨l, hfN⟩ := hfN
let kl := max k l
replace hfM : fM ^ kl = 0 := pow_eq_zero_of_le (by omega) hfM
replace hfN : fN ^ kl = 0 := pow_eq_zero_of_le (by omega) hfN
have (i : ℕ) : (fN ^ i) (g m) = g ((fM ^ i) m) := by
simpa using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h i) m
simp [exp_eq_sum hfM, exp_eq_sum hfN, this, map_rat_smul]
