Derivations #
This file defines derivation. A derivation D
from the R
-algebra A
to the A
-module M
is an
R
-linear map that satisfy the Leibniz rule D (a * b) = a * D b + D a * b
.
Main results #
Derivation
: The type ofR
-derivations fromA
toM
. This has anA
-module structure.Derivation.llcomp
: We may compose linear maps and derivations to obtain a derivation, and the composition is bilinear.
See RingTheory.Derivation.Lie
for
derivation.lie_algebra
: TheR
-derivations fromA
toA
form a lie algebra overR
.
and RingTheory.Derivation.ToSquareZero
for
derivation_to_square_zero_equiv_lift
: TheR
-derivations fromA
into a square-zero idealI
ofB
corresponds to the liftsA →ₐ[R] B
of the mapA →ₐ[R] B ⧸ I
.
Future project #
- Generalize derivations into bimodules.
- toFun : A → M
- map_add' : ∀ (x y : A), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : A), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_one_eq_zero' : ↑↑s 1 = 0
D : Derivation R A M
is an R
-linear map from A
to M
that satisfies the leibniz
equality. We also require that D 1 = 0
. See Derivation.mk'
for a constructor that deduces this
assumption from the Leibniz rule when M
is cancellative.
TODO: update this when bimodules are defined.
Instances For
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal on the whole algebra.
coe_fn
as an AddMonoidHom
.
Instances For
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.
Instances For
The composition of a derivation with a linear map as a bilinear map
Instances For
Pushing a derivation forward through a linear equivalence is an equivalence.
Instances For
If A
is both an R
-algebra and an S
-algebra; M
is both an R
-module and an S
-module,
then an S
-derivation A → M
is also an R
-derivation if it is also R
-linear.
Instances For
Define Derivation R A M
from a linear map when M
is cancellative by verifying the Leibniz
rule.