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.

Main results #

Future project #

structure derivation (R : Type u_1) (A : Type u_2) [comm_semiring R] [comm_semiring A] [algebra R A] (M : Type u_3) [add_comm_monoid M] [module A M] [module R 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. 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 derivation
@[protected, instance]
def derivation.add_monoid_hom_class {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
Equations
@[protected, 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_comm_monoid M] [module A M] [module R M] :
has_coe_to_fun (derivation R A M) (λ (_x : derivation R A M), A M)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) :
@[protected, 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] (f : A →ₗ[R] M) (h₁ : f 1 = 0) (h₂ : (a b : A), f (a * b) = a f b + b f a) :
@[simp, norm_cast]
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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (h : D1 = D2) (a : A) :
D1 a = D2 a
@[protected]
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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a b : A) :
D (a + b) = D a + D b
@[protected]
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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a b : A) :
D (a * b) = a D b + b D a
theorem derivation.map_sum {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {ι : Type u_4} (s : finset ι) (f : ι A) :
D (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), D (f i))
@[simp]
theorem derivation.map_smul_of_tower {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [has_smul S A] [has_smul S M] [linear_map.compatible_smul A M S R] (D : derivation R A M) (r : S) (a : A) :
D (r a) = r 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (r : R) :
D ((algebra_map R A) r) = 0
@[simp]
theorem derivation.map_coe_nat {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (n : ) :
D n = 0
@[simp]
theorem derivation.leibniz_pow {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a : A) (n : ) :
D (a ^ n) = n a ^ (n - 1) D a
theorem derivation.eq_on_adjoin {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} {s : set A} (h : set.eq_on D1 D2 s) :
theorem derivation.ext_of_adjoin_eq_top {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (s : set A) (hs : algebra.adjoin R s = ) (h : set.eq_on D1 D2 s) :
D1 = D2

If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal on the whole algebra.

@[protected, 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] (a : A) :
0 a = 0
@[protected, 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R 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_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (a : A) :
(D1 + D2) a = D1 a + D2 a
@[protected, 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_comm_monoid M] [module A M] [module R M] :
Equations
@[protected, instance]
def derivation.has_smul {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S 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_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
(r D) = r 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_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
(r D) = r 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_comm_monoid M] [module A M] [module R M] (a : A) {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
(r D) a = r D a
@[protected, instance]
@[protected, instance]
def derivation.module {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [semiring S] [module S M] [smul_comm_class R S M] [smul_comm_class S A M] :
module S (derivation R A M)
Equations
@[protected, 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_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_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [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_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
def derivation.llcomp {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] :

The composition of a derivation with a linear map as a bilinear map

Equations
@[simp]
theorem derivation.llcomp_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
def linear_equiv.comp_der {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (e : M ≃ₗ[A] N) :

Pushing a derivation foward through a linear equivalence is an equivalence.

Equations
@[protected]
def derivation.restrict_scalars (R : Type u_1) [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [comm_semiring S] [algebra S A] [module S M] [linear_map.compatible_smul A M R S] (d : derivation S A M) :

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.

Equations
def derivation.mk' {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 R M] [module A M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :

Define derivation R A M from a linear map when M is cancellative by verifying the Leibniz rule.

Equations
@[simp]
theorem derivation.coe_mk' {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 R M] [module A M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :
@[simp]
theorem derivation.coe_mk'_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 R M] [module A M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :
@[protected]
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] (D : derivation R A M) (a : A) :
D (-a) = -D a
@[protected]
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] (D : derivation R A M) (a b : A) :
D (a - b) = D a - D b
@[simp]
theorem derivation.map_coe_int {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] (D : derivation R A M) (n : ) :
D n = 0
theorem derivation.leibniz_of_mul_eq_one {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] (D : derivation R A M) {a b : A} (h : a * b = 1) :
D a = -a ^ 2 D b
theorem derivation.leibniz_inv_of {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] (D : derivation R A M) (a : A) [invertible a] :
D ( a) = - a ^ 2 D a
theorem derivation.leibniz_inv {R : Type u_1} [comm_ring R] {M : Type u_3} [add_comm_group M] [module R M] {K : Type u_2} [field K] [module K M] [algebra R K] (D : derivation R K M) (a : K) :
@[protected, 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] :
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] (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] (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] (D : derivation R A M) (a : A) :
(-D) a = -D a
@[protected, 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] :
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] (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] (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] {D1 D2 : derivation R A M} (a : A) :
(D1 - D2) a = D1 a - D2 a
@[protected, 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] :
Equations

Lie structures #

@[protected, 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)
def diff_to_ideal_of_quotient_comp_eq {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R I).comp f₂) :

If f₁ f₂ : A →ₐ[R] B are two lifts of the same A →ₐ[R] B ⧸ I, we may define a map f₁ - f₂ : A →ₗ[R] I.

Equations
@[simp]
theorem diff_to_ideal_of_quotient_comp_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R I).comp f₂) (x : A) :
((diff_to_ideal_of_quotient_comp_eq I f₁ f₂ e) x) = f₁ x - f₂ x
def derivation_to_square_zero_of_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B I)) :

Given a tower of algebras R → A → B, and a square-zero I : ideal B, each lift A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I corresponds to a R-derivation from A to I.

Equations
theorem derivation_to_square_zero_of_lift_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B I)) (x : A) :
def lift_of_derivation_to_square_zero {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : derivation R A I) :

Given a tower of algebras R → A → B, and a square-zero I : ideal B, each R-derivation from A to I corresponds to a lift A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I.

Equations
theorem lift_of_derivation_to_square_zero_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : derivation R A I) (x : A) :
@[simp]
theorem lift_of_derivation_to_square_zero_mk_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (d : derivation R A I) (x : A) :
def derivation_to_square_zero_equiv_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] :

Given a tower of algebras R → A → B, and a square-zero I : ideal B, there is a 1-1 correspondance between R-derivations from A to I and lifts A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I.

Equations
@[reducible]
def kaehler_differential.ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :

The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

def derivation.tensor_product_to {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {M : Type u_3} [add_comm_group M] [module R M] [module S M] [is_scalar_tower R S M] (D : derivation R S M) :

For a R-derivation S → M, this is the map S ⊗[R] S →ₗ[S] M sending s ⊗ₜ t ↦ s • D t.

Equations
theorem derivation.tensor_product_to_tmul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {M : Type u_3} [add_comm_group M] [module R M] [module S M] [is_scalar_tower R S M] (D : derivation R S M) (s t : S) :

The kernel of S ⊗[R] S →ₐ[R] S is generated by 1 ⊗ s - s ⊗ 1 as a S-module.

def kaehler_differential (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :
Type u_2

The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use kaehler_differential.tensor_product_to_surjective and derivation.tensor_product_to_tmul.

We also provide the notation Ω[S⁄R] for kaehler_differential R S. Note that the slash is \textfractionsolidus.

Equations
Instances for kaehler_differential
@[protected, instance]
def kaehler_differential.module (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :
@[protected, instance]
@[protected, instance]
def kaehler_differential.nonempty (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :
@[protected, instance]
def kaehler_differential.module' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_3} [comm_ring R'] [algebra R' S] :
Equations
@[protected, instance]
@[protected, instance]
def kaehler_differential.is_scalar_tower_of_tower (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] {R₁ : Type u_3} {R₂ : Type u_4} [comm_ring R₁] [comm_ring R₂] [algebra R₁ S] [algebra R₂ S] [algebra R₁ R₂] [is_scalar_tower R₁ R₂ S] :
@[protected, instance]

The quotient map I → Ω[S⁄R] with I being the kernel of S ⊗[R] S → S.

Equations
def kaehler_differential.D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :

The universal derivation into Ω[S⁄R].

Equations
def derivation.lift_kaehler_differential {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {M : Type u_3} [add_comm_group M] [module R M] [module S M] [is_scalar_tower R S M] (D : derivation R S M) :

The linear map from Ω[S⁄R], associated with a derivation.

Equations
@[simp]
theorem derivation.lift_kaehler_differential_comp_D {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {M : Type u_3} [add_comm_group M] [module R M] [module S M] [is_scalar_tower R S M] (D' : derivation R S M) (x : S) :
@[ext]
theorem derivation.lift_kaehler_differential_unique {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {M : Type u_3} [add_comm_group M] [module R M] [module S M] [is_scalar_tower R S M] (f f' : Ω[SR] →ₗ[S] M) (hf : (f.comp_der) (kaehler_differential.D R S) = (f'.comp_der) (kaehler_differential.D R S)) :
f = f'

The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations from S to M.

Equations

The endomorphisms of Ω[S⁄R] corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S, with J being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

Equations
noncomputable def kaehler_differential.ker_total (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] :

The S-submodule of S →₀ S (the direct sum of copies of S indexed by S) generated by the relations:

  1. dx + dy = d(x + y)
  2. x dy + y dx = d(x * y)
  3. dr = 0 for r ∈ R where db is the unit in the copy of S with index b.

This is the kernel of the surjection finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S). See kaehler_differential.ker_total_eq and kaehler_differential.total_surjective.

Equations

The (universal) derivation into (S →₀ S) ⧸ kaehler_differential.ker_total R S.

Equations
def derivation.comp_algebra_map {R : Type u_1} [comm_ring R] {M : Type u_3} [add_comm_group M] [module R M] (A : Type u_4) {B : Type u_5} [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] [module A M] [module B M] [is_scalar_tower A B M] (d : derivation R B M) :

For a tower R → A → B and an R-derivation B → M, we may compose with A → B to obtain an R-derivation A → M.

Equations
def kaehler_differential.map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [algebra S B] [is_scalar_tower R A B] [is_scalar_tower R S B] :

The map Ω[A⁄R] →ₗ[A] Ω[B⁄R] given a square A --→ B ↑ ↑ | | R --→ S

Equations
theorem kaehler_differential.map_D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [algebra S B] [is_scalar_tower R A B] [is_scalar_tower R S B] (x : A) :
noncomputable def kaehler_differential.map_base_change (R : Type u_1) [comm_ring R] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] :

The lift of the map Ω[A⁄R] →ₗ[A] Ω[B⁄R] to the base change along A → B. This is the first map in the exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0.

Equations
@[simp]
theorem kaehler_differential.map_base_change_tmul (R : Type u_1) [comm_ring R] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x : B) (y : Ω[AR]) :