English
For a derivation d : Derivation R A M and a ∈ A, the derivation compAEval a : Derivation R R[X] (Module.AEval R M a) is defined by f ↦ AEval.of R M a (d (aeval a f)).
Русский
Для выводной операции d и элемента a ∈ A, определено новое выводное отображение compAEval a: Derivation R R[X] Module.AEval R M a как f ↦ AEval.of R M a (d (aeval a f)).
LaTeX
$$$\\text{compAEval} : \\mathrm{Derivation}\\; R\\; R[X] \\lvert \\mathrm{AEval}\\; R\\; M\\; a \\to \\mathrm{AEval}\\; R\\; M \\; a$$ with $ (\\mathrm{compAEval}\; d\; a)(f) = \\mathrm{AEval.of}\\ R\\; M\\ a \\bigl(d(\\mathrm{aeval}\\ a\\; f)\\bigr) $$$
Lean4
/-- For a derivation `d : A → M` and an element `a : A`, `d.compAEval a` is the
derivation of `R[X]` which takes a polynomial `f` to `d(aeval a f)`.
This derivation takes values in `Module.AEval R M a`, which is `M`, regarded as an
`R[X]`-module, with the action of a polynomial `f` defined by `f • m = (aeval a f) • m`.
-/
/-
Note: `compAEval` is not defined using `Derivation.compAlgebraMap`.
This because `A` is not an `R[X]` algebra and it would be messy to create an algebra instance
within the definition.
-/
@[simps]
def compAEval : Derivation R R[X] <| AEval R M a
where
toFun f := AEval.of R M a (d (aeval a f))
map_add' := by simp
map_smul' := by simp
leibniz' := by simp [AEval.of_aeval_smul, -Derivation.map_aeval]
map_one_eq_zero' := by simp
