mathlib documentation

ring_theory.derivation

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.

def derivation.to_linear_map {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] [module A M] [module R M] [is_scalar_tower R A M] (self : derivation R A M) :

The linear_map underlying a derivation.

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] [module A M] [module R M] [is_scalar_tower R A M] :
Type (max u_2 u_3)

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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) :
@[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] [module A M] [module R M] [is_scalar_tower R A M] :
has_coe (derivation R A M) (A →ₗ[R] M)
Equations
@[simp]
theorem derivation.to_linear_map_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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) :
@[simp]
theorem derivation.mk_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] [module A M] [module R M] [is_scalar_tower R A M] (f : A →ₗ[R] M) (h₁ : ∀ (x y : A), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : A), f (m x) = m f x) (h₃ : ∀ (a b : A), f (a * b) = a f b + b f a) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, leibniz' := h₃} = f
@[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] [module A M] [module 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] [module A M] [module R M] [is_scalar_tower 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] [module A M] [module R M] [is_scalar_tower R A M] {D1 D2 : derivation R A M} (H : ∀ (a : A), D1 a = D2 a) :
D1 = D2
theorem derivation.congr_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] [module A M] [module R M] [is_scalar_tower R A M] {D1 D2 : derivation R A M} (h : D1 = D2) (a : A) :
D1 a = D2 a
@[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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) (a b : A) :
D (a + b) = D a + D b
@[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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) :
D 0 = 0
@[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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) (r : R) (a : A) :
D (r a) = r D 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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) (a b : A) :
D (a * b) = a D b + b D 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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) :
D 1 = 0
@[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] [module A M] [module 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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[simp]
theorem derivation.coe_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] [module A M] [module R M] [is_scalar_tower R A M] :
0 = 0
@[simp]
theorem derivation.coe_zero_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] [module A M] [module R M] [is_scalar_tower R A M] :
0 = 0
theorem derivation.zero_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] [module A M] [module R M] [is_scalar_tower R A M] (a : A) :
0 a = 0
@[instance]
def derivation.has_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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[simp]
theorem derivation.coe_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] [module A M] [module R M] [is_scalar_tower R A M] (D1 D2 : derivation R A M) :
(D1 + D2) = D1 + D2
@[simp]
theorem derivation.coe_add_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] [module A M] [module R M] [is_scalar_tower R A M] (D1 D2 : derivation R A M) :
(D1 + D2) = D1 + D2
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] [module A M] [module R M] [is_scalar_tower R A M] {D1 D2 : derivation R A M} (a : A) :
(D1 + D2) a = D1 a + D2 a
@[instance]
def derivation.Rscalar {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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[simp]
theorem derivation.coe_Rsmul {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] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (D : derivation R A M) :
(r D) = r D
@[simp]
theorem derivation.coe_Rsmul_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] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (D : derivation R A M) :
(r D) = r D
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] [module A M] [module R M] [is_scalar_tower R A M] (a : A) (r : R) (D : derivation R A M) :
(r D) a = r D a
@[instance]
def derivation.has_scalar {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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[simp]
theorem derivation.coe_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] [module A M] [module R M] [is_scalar_tower R A M] (a : A) (D : derivation R A M) :
(a D) = a D
@[simp]
theorem derivation.coe_smul_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] [module A M] [module R M] [is_scalar_tower R A M] (a : A) (D : derivation R A M) :
(a D) = a D
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] [module A M] [module R M] [is_scalar_tower R A M] (a : A) (D : derivation R A M) (b : A) :
(a D) b = a D b
@[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] [module A M] [module R M] [is_scalar_tower R A M] :
Equations
@[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] [module A M] [module R M] [is_scalar_tower R A M] :
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] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_cancel_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :

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.

Equations
@[simp]
theorem derivation.coe_to_linear_map_comp {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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) {N : Type u_4} [add_cancel_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
@[simp]
theorem derivation.coe_comp {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] [module A M] [module R M] [is_scalar_tower R A M] (D : derivation R A M) {N : Type u_4} [add_cancel_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
@[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) :
D (-a) = -D 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) :
D (a - b) = D a - D b
@[instance]
def derivation.has_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] :
Equations
@[simp]
theorem derivation.coe_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) :
@[simp]
theorem derivation.coe_neg_linear_map {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) :
theorem derivation.neg_apply {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) :
(-D) a = -D a
@[instance]
def derivation.has_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] :
Equations
@[simp]
theorem derivation.coe_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] (D1 D2 : derivation R A M) :
(D1 - D2) = D1 - D2
@[simp]
theorem derivation.coe_sub_linear_map {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] (D1 D2 : derivation R A M) :
(D1 - D2) = D1 - D2
theorem derivation.sub_apply {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] {D1 D2 : derivation R A M} (a : A) :
(D1 - D2) a = D1 a - D2 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] :
Equations

Lie structures #

@[instance]
def derivation.has_bracket {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :

The commutator of derivations is again a derivation.

Equations
@[simp]
theorem derivation.commutator_coe_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} :
theorem derivation.commutator_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} (a : A) :
D1,D2 a = D1 (D2 a) - D2 (D1 a)
@[instance]
def derivation.lie_ring {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :
Equations