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.
Notation
The notation ⁅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.
structure
derivation
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(M : Type u_3)
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
Type (max u_2 u_3)
- to_linear_map : A →ₗ[R] M
- leibniz' : ∀ (a b : A), c.to_linear_map.to_fun (a * b) = a • c.to_linear_map.to_fun b + b • c.to_linear_map.to_fun a
D : derivation R A M is an R-linear map from A to M that satisfies the leibniz
equality.
TODO: update this when bimodules are defined.
@[instance]
def
derivation.has_coe_to_fun
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
has_coe_to_fun (derivation R A M)
Equations
- derivation.has_coe_to_fun = {F := λ (D : derivation R A M), A → M, coe := λ (D : derivation R A M), D.to_linear_map.to_fun}
@[instance]
def
derivation.has_coe_to_linear_map
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
has_coe (derivation R A M) (A →ₗ[R] M)
Equations
- derivation.has_coe_to_linear_map = {coe := λ (D : derivation R A M), D.to_linear_map}
@[simp]
theorem
derivation.to_fun_eq_coe
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M) :
D.to_linear_map.to_fun = ⇑D
@[simp]
theorem
derivation.coe_fn_coe
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(f : derivation R A M) :
theorem
derivation.coe_injective
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
{D1 D2 : derivation R A M} :
@[ext]
theorem
derivation.ext
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
{D1 D2 : derivation R A M} :
@[simp]
theorem
derivation.map_add
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(a b : A) :
@[simp]
theorem
derivation.map_zero
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M) :
@[simp]
theorem
derivation.map_smul
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(r : R)
(a : A) :
@[simp]
theorem
derivation.leibniz
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(a b : A) :
@[simp]
theorem
derivation.map_one_eq_zero
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M) :
@[simp]
theorem
derivation.map_algebra_map
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(r : R) :
⇑D (⇑(algebra_map R A) r) = 0
@[instance]
def
derivation.has_zero
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
has_zero (derivation R A M)
Equations
- derivation.has_zero = {zero := {to_linear_map := 0, leibniz' := _}}
@[instance]
def
derivation.inhabited
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
inhabited (derivation R A M)
Equations
- derivation.inhabited = {default := 0}
@[instance]
def
derivation.add_comm_monoid
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
add_comm_monoid (derivation R A M)
@[simp]
theorem
derivation.add_apply
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
{D1 D2 : derivation R A M}
(a : A) :
@[instance]
def
derivation.derivation.Rsemimodule
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
semimodule R (derivation R A M)
Equations
- derivation.derivation.Rsemimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (r : R) (D : derivation R A M), {to_linear_map := r • ↑D, leibniz' := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
derivation.smul_to_linear_map_coe
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(r : R) :
@[simp]
theorem
derivation.Rsmul_apply
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(r : R)
(a : A) :
@[instance]
def
derivation.semimodule
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
semimodule A (derivation R A M)
Equations
- derivation.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (a : A) (D : derivation R A M), {to_linear_map := {to_fun := λ (b : A), a • ⇑D b, map_add' := _, map_smul' := _}, leibniz' := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
derivation.smul_apply
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(a b : A) :
@[instance]
def
derivation.is_scalar_tower
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M] :
is_scalar_tower R A (derivation R A M)
Equations
@[simp]
theorem
derivation.map_neg
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A]
{M : Type u_3}
[add_comm_group M]
[module A M]
[module R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(a : A) :
@[simp]
theorem
derivation.map_sub
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A]
{M : Type u_3}
[add_comm_group M]
[module A M]
[module R M]
[is_scalar_tower R A M]
(D : derivation R A M)
(a b : A) :
@[instance]
def
derivation.add_comm_group
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A]
{M : Type u_3}
[add_comm_group M]
[module A M]
[module R M]
[is_scalar_tower R A M] :
add_comm_group (derivation R A M)
Equations
- derivation.add_comm_group = {add := add_comm_monoid.add derivation.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero derivation.add_comm_monoid, zero_add := _, add_zero := _, neg := λ (D : derivation R A M), {to_linear_map := -↑D, leibniz' := _}, add_left_neg := _, add_comm := _}
Lie structures
def
derivation.commutator
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A] :
derivation R A A → derivation R A A → derivation R A A
The commutator of derivations is again a derivation.
Equations
- D1.commutator D2 = {to_linear_map := ⁅↑D1,↑D2⁆, leibniz' := _}
@[instance]
def
derivation.has_bracket
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A] :
has_bracket (derivation R A A)
Equations
- derivation.has_bracket = {bracket := derivation.commutator _inst_3}
@[instance]
def
derivation.lie_ring
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A] :
lie_ring (derivation R A A)
Equations
- derivation.lie_ring = {to_add_comm_group := derivation.add_comm_group derivation.lie_ring._proof_3, to_has_bracket := derivation.has_bracket _inst_3, add_lie := _, lie_add := _, lie_self := _, jacobi := _}
@[instance]
def
derivation.lie_algebra
{R : Type u_1}
[comm_ring R]
{A : Type u_2}
[comm_ring A]
[algebra R A] :
lie_algebra R (derivation R A A)
Equations
def
linear_map.comp_der
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
{N : Type u_4}
[add_cancel_comm_monoid N]
[semimodule A N]
[semimodule R N]
[is_scalar_tower R A M]
[is_scalar_tower R A N] :
(M →ₗ[A] N) → derivation R A M → derivation R A N
The composition of a linear map and a derivation is a derivation.
@[simp]
theorem
linear_map.comp_der_apply
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[comm_semiring A]
[algebra R A]
{M : Type u_3}
[add_cancel_comm_monoid M]
[semimodule A M]
[semimodule R M]
{N : Type u_4}
[add_cancel_comm_monoid N]
[semimodule A N]
[semimodule R N]
[is_scalar_tower R A M]
[is_scalar_tower R A N]
(f : M →ₗ[A] N)
(D : derivation R A M)
(a : A) :