This file defines derivation. A derivation
D from the
A to the
M is an
R-linear map that satisfy the Leibniz rule
D (a * b) = a * D b + D a * b.
⁅D1, D2⁆ is used for the commutator of two derivations.
TODO: this file is just a stub to go on with some PRs in the geometry section. It only implements the definition of derivations in commutative algebra. This will soon change: as soon as bimodules will be there in mathlib I will change this file to take into account the non-commutative case. Any development on the theory of derivations is discouraged until the definitive definition of derivation will be implemented.
- to_fun : A → M
- map_add' : ∀ (x y : A), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (m : R) (x : A), c.to_fun (m • x) = m • c.to_fun x
- leibniz' : ∀ (a b : A), c.to_fun (a * b) = a • c.to_fun b + b • c.to_fun a
D : derivation R A M is an
R-linear map from
M that satisfies the
TODO: update this when bimodules are defined.
We can push forward derivations using linear maps, i.e., the composition of a derivation with a linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations.
Lie structures #
The commutator of derivations is again a derivation.