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_linear_map : A →ₗ[R] M
- leibniz' : ∀ (a b : A), self.to_linear_map.to_fun (a * b) = a • self.to_linear_map.to_fun b + b • self.to_linear_map.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.
If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal on the whole algebra.
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.