English
Let f: R →ₐ[A] R' be an injective A-algebra homomorphism between differential algebras, and let x ∈ R be separable over A. Then f(x′) = (f x)′, i.e., derivations commute with f on separable elements.
Русский
Пусть f: R →ₐ[A] R' — инъективное A-алгебровое отображение между дифференциальными алгебрами, и пусть x ∈ R является разделимым над A. Тогда f(x′) = (f x)′, то есть производная сохраняется под отображением.
LaTeX
$$$\forall \{A : Type\*\} [\mathrm{CommRing} A] [\mathrm{Differential } A] {R : Type\*} [\mathrm{CommRing} R] [\mathrm{Differential } R] [Algebra A R] {R' : Type\*} [\mathrm{CommRing} R'] [\mathrm{Differential } R'] [Algebra A R'] [\mathrm{IsDomain} R'] [IsSeparable A R] (f : R \toₐ[A] R') (hf : Function.Injective f) (x : R) (h : IsSeparable A x),
f(x′) = (f x)′$$$
Lean4
theorem algHom_deriv (f : R →ₐ[A] R') (hf : Function.Injective f) (x : R) (h : IsSeparable A x) : f (x′) = (f x)′ :=
by
let p := minpoly A x
apply mul_left_cancel₀ (a := aeval (f x) (derivative p))
· rw [Polynomial.aeval_algHom]
simp only [AlgHom.coe_comp, Function.comp_apply, ne_eq, map_eq_zero_iff f hf]
apply Separable.aeval_derivative_ne_zero h (minpoly.aeval A x)
conv => lhs; rw [Polynomial.aeval_algHom]
simp only [AlgHom.coe_comp, Function.comp_apply, ← map_mul]
apply add_left_cancel (a := aeval (f x) (mapCoeffs p))
rw [← deriv_aeval_eq]
simp only [aeval_algHom, AlgHom.coe_comp, Function.comp_apply, ← map_add, ← deriv_aeval_eq, minpoly.aeval, map_zero,
p]
