# mathlibdocumentation

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 #

• `derivation`: The type of `R`-derivations from `A` to `M`. This has an `A`-module structure.
• `derivation.llcomp`: We may compose linear maps and derivations to obtain a derivation, and the composition is bilinear.
• `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form an lie algebra over `R`.
• `derivation_to_square_zero_equiv_lift`: The `R`-derivations from `A` into a square-zero ideal `I` of `B` corresponds to the lifts `A →ₐ[R] B` of the map `A →ₐ[R] B ⧸ I`.
• `kaehler_differential`: The module of kaehler differentials. For an `R`-algebra `S`, we provide the notation `Ω[S⁄R]` for `kaehler_differential R S`. Note that the slash is `\textfractionsolidus`.
• `kaehler_differential.D`: The derivation into the module of kaehler differentials.
• `kaehler_differential.span_range_derivation`: The image of `D` spans `Ω[S⁄R]` as an `S`-module.
• `kaehler_differential.linear_map_equiv_derivation`: The isomorphism `Hom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M)`.
• `kaehler_differential.quot_ker_total_equiv`: An alternative description of `Ω[S⁄R]` as `S` copies of `S` with kernel (`kaehler_differential.ker_total`) generated by the relations:
1. `dx + dy = d(x + y)`
2. `x dy + y dx = d(x * y)`
3. `dr = 0` for `r ∈ R`
• `kaehler_differential.map`: Given a map between the arrows `R → A` and `S → B`, we have an `A`-linear map `Ω[A⁄R] → Ω[B⁄S]`.

## Future project #

• Generalize derivations into bimodules.
• Define a `is_kaehler_differential` predicate.
structure derivation (R : Type u_1) (A : Type u_2) [ A] (M : Type u_3) [ M] [ 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
Equations
@[protected, instance]
def derivation.has_coe_to_fun {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
has_coe_to_fun A M) (λ (_x : 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) :
@[protected, instance]
def derivation.has_coe_to_linear_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
has_coe A M) (A →ₗ[R] M)
Equations
@[simp]
theorem derivation.to_linear_map_eq_coe {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) :
@[simp]
theorem derivation.mk_coe {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (f : A M) :
theorem derivation.coe_injective {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
@[ext]
theorem derivation.ext {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {D1 D2 : A M} (H : (a : A), D1 a = D2 a) :
D1 = D2
theorem derivation.congr_fun {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {D1 D2 : A M} (h : D1 = D2) (a : A) :
D1 a = D2 a
@[protected]
theorem derivation.map_add {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (a b : A) :
D (a + b) = D a + D b
@[protected]
theorem derivation.map_zero {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) :
D 0 = 0
@[simp]
theorem derivation.map_smul {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (r : R) (a : A) :
D (r a) = r D a
@[simp]
theorem derivation.leibniz {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (a b : A) :
D (a * b) = a D b + b D a
theorem derivation.map_sum {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [ A] [ M] [ R] (D : A M) (r : S) (a : A) :
D (r a) = r D a
@[simp]
theorem derivation.map_one_eq_zero {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) :
D 1 = 0
@[simp]
theorem derivation.map_algebra_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (r : R) :
D ( A) r) = 0
@[simp]
theorem derivation.map_coe_nat {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (n : ) :
D n = 0
@[simp]
theorem derivation.leibniz_pow {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) (a : A) (n : ) :
D (a ^ n) = n a ^ (n - 1) D a
theorem derivation.eq_on_adjoin {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {D1 D2 : A M} {s : set A} (h : D2 s) :
D2 s)
theorem derivation.ext_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {D1 D2 : A M} (s : set A) (hs : = ) (h : 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
Equations
@[simp]
theorem derivation.coe_zero {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
0 = 0
@[simp]
theorem derivation.coe_zero_linear_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
0 = 0
theorem derivation.zero_apply {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (a : A) :
0 a = 0
@[protected, instance]
def derivation.has_add {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
Equations
@[simp]
theorem derivation.coe_add {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D1 D2 : A M) :
(D1 + D2) = D1 + D2
@[simp]
theorem derivation.coe_add_linear_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D1 D2 : A M) :
(D1 + D2) = D1 + D2
theorem derivation.add_apply {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {D1 D2 : A M} (a : A) :
(D1 + D2) a = D1 a + D2 a
@[protected, instance]
def derivation.inhabited {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
Equations
@[protected, instance]
def derivation.has_smul {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [monoid S] [ M] [ M] [ M] :
A M)
Equations
@[simp]
theorem derivation.coe_smul {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [monoid S] [ M] [ M] [ M] (r : S) (D : A M) :
(r D) = r D
@[simp]
theorem derivation.coe_smul_linear_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [monoid S] [ M] [ M] [ M] (r : S) (D : A M) :
(r D) = r D
theorem derivation.smul_apply {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (a : A) {S : Type u_4} [monoid S] [ M] [ M] [ M] (r : S) (D : A M) :
(r D) a = r D a
@[protected, instance]
def derivation.add_comm_monoid {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
Equations
def derivation.coe_fn_add_monoid_hom {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] :
A M →+ A M

`coe_fn` as an `add_monoid_hom`.

Equations
@[protected, instance]
def derivation.distrib_mul_action {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [monoid S] [ M] [ M] [ M] :
A M)
Equations
@[protected, instance]
def derivation.is_central_scalar {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [monoid S] [ M] [ M] [ M] [ M] :
A M)
@[protected, instance]
def derivation.module {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [semiring S] [ M] [ M] [ M] :
A M)
Equations
@[protected, instance]
def derivation.is_scalar_tower {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] [ M] :
A M)
def linear_map.comp_der {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {N : Type u_4} [ N] [ N] [ M] [ N] (f : M →ₗ[A] N) :
A M →ₗ[R] 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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) {N : Type u_4} [ N] [ N] [ M] [ N] (f : M →ₗ[A] N) :
@[simp]
theorem derivation.coe_comp {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A M) {N : Type u_4} [ N] [ N] [ M] [ N] (f : M →ₗ[A] N) :
def derivation.llcomp {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {N : Type u_4} [ N] [ N] [ M] [ N] :
(M →ₗ[A] N) →ₗ[A] A M →ₗ[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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {N : Type u_4} [ N] [ N] [ M] [ N] (f : M →ₗ[A] N) :
def linear_equiv.comp_der {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {N : Type u_4} [ N] [ N] [ M] [ N] (e : M ≃ₗ[A] N) :
A M ≃ₗ[R] A N

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

Equations
@[protected]
def derivation.restrict_scalars (R : Type u_1) {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] {S : Type u_4} [ A] [ M] [ S] (d : A M) :
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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :
A M

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} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :
h) = D
@[simp]
theorem derivation.coe_mk'_linear_map {R : Type u_1} {A : Type u_2} [ A] {M : Type u_3} [ M] [ M] (D : A →ₗ[R] M) (h : (a b : A), D (a * b) = a D b + b D a) :
h) = D
@[protected]
theorem derivation.map_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] (D : 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] [ A] {M : Type u_3} [ M] [ M] (D : 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] [ A] {M : Type u_3} [ M] [ M] (D : 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] [ A] {M : Type u_3} [ M] [ M] (D : 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] [ A] {M : Type u_3} [ M] [ M] (D : 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} [ M] {K : Type u_2} [field K] [ M] [ K] (D : K M) (a : K) :
@[protected, instance]
def derivation.has_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] :
has_neg A M)
Equations
@[simp]
theorem derivation.coe_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] (D : A M) :
@[simp]
theorem derivation.coe_neg_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] (D : A M) :
theorem derivation.neg_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] (D : 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] [ A] {M : Type u_3} [ M] [ M] :
has_sub A M)
Equations
@[simp]
theorem derivation.coe_sub {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] (D1 D2 : 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] [ A] {M : Type u_3} [ M] [ M] (D1 D2 : A M) :
(D1 - D2) = D1 - D2
theorem derivation.sub_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {M : Type u_3} [ M] [ M] {D1 D2 : 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] [ A] {M : Type u_3} [ M] [ M] :
Equations

# Lie structures #

@[protected, instance]
def derivation.has_bracket {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] :
has_bracket A A) A 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] [ A] {D1 D2 : A A} :
theorem derivation.commutator_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {D1 D2 : A A} (a : A) :
D1, D2 a = D1 (D2 a) - D2 (D1 a)
@[protected, instance]
def derivation.lie_ring {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] :
Equations
@[protected, instance]
def derivation.lie_algebra {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] :
A A)
Equations
def diff_to_ideal_of_quotient_comp_eq {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : I).comp f₁ = 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
• e = _
@[simp]
theorem diff_to_ideal_of_quotient_comp_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : I).comp f₁ = I).comp f₂) (x : A) :
( e) x) = f₁ x - f₂ x
def derivation_to_square_zero_of_lift {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A →ₐ[R] B) (e : I).comp f = (B I)) :
A 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_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A →ₐ[R] B) (e : I).comp f = (B I)) (x : A) :
( e) x) = f x - B) x
def lift_of_derivation_to_square_zero {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : 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_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A I) (x : A) :
x = (f x) + B) x
@[simp]
theorem lift_of_derivation_to_square_zero_mk_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (d : A I) (x : A) :
( x) = (B I)) x
def derivation_to_square_zero_equiv_lift {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] :
A I {f // I).comp f = (B I)}

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
@[simp]
theorem derivation_to_square_zero_equiv_lift_symm_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : {f // I).comp f = (B I)}) :
f = _
@[simp]
theorem derivation_to_square_zero_equiv_lift_apply_coe {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (d : A I) :
d) =
@[reducible]
def kaehler_differential.ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
ideal S S)

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

theorem kaehler_differential.one_smul_sub_smul_one_mem_ideal (R : Type u_1) {S : Type u_2} [comm_ring R] [comm_ring S] [ S] (a : S) :
1 ⊗ₜ[R] a - a ⊗ₜ[R] 1
def derivation.tensor_product_to {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :
S →ₗ[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] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (s t : S) :
theorem derivation.tensor_product_to_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (x y : S) :
theorem kaehler_differential.submodule_span_range_eq_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
(set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) =

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

theorem kaehler_differential.span_range_eq_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
ideal.span (set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) =
def kaehler_differential (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ 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] [ S] :
@[protected, instance]
def kaehler_differential.add_comm_group (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[protected, instance]
def kaehler_differential.nonempty (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[protected, instance]
def kaehler_differential.module' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {R' : Type u_3} [comm_ring R'] [algebra R' S] :
Equations
@[protected, instance]
def kaehler_differential.is_scalar_tower (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S S) Ω[SR]
@[protected, instance]
def kaehler_differential.is_scalar_tower_of_tower (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {R₁ : Type u_3} {R₂ : Type u_4} [comm_ring R₁] [comm_ring R₂] [algebra R₁ S] [algebra R₂ S] [algebra R₁ R₂] [ R₂ S] :
R₂ Ω[SR]
@[protected, instance]
def kaehler_differential.is_scalar_tower' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S S) Ω[SR]
def kaehler_differential.from_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :

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

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

(Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`.

Equations
theorem kaehler_differential.D_linear_map_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (s : S) :
= 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
def kaehler_differential.D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S Ω[SR]

The universal derivation into `Ω[S⁄R]`.

Equations
theorem kaehler_differential.D_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (s : S) :
s = 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
theorem kaehler_differential.span_range_derivation (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
def derivation.lift_kaehler_differential {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :

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

Equations
theorem derivation.lift_kaehler_differential_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (x : ) :
theorem derivation.lift_kaehler_differential_comp {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :
@[simp]
theorem derivation.lift_kaehler_differential_comp_D {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D' : 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] [ S] {M : Type u_3} [ M] [ M] [ M] (f f' : Ω[SR] →ₗ[S] M) (hf : (f.comp_der) = (f'.comp_der) ) :
f = f'
theorem derivation.lift_kaehler_differential_D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
theorem kaehler_differential.D_tensor_product_to {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] (x : ) :
= x
def kaehler_differential.linear_map_equiv_derivation (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] :

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

Equations

The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S`.

Equations

The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S` as an `S`-algebra.

Equations
theorem kaehler_differential.End_equiv_aux (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (f : S →ₐ[R] S ) :
= S S
noncomputable def kaehler_differential.End_equiv_derivation' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S Ω[SR] ≃ₗ[R] S

Derivations into `Ω[S⁄R]` is equivalent to derivations into `(kaehler_differential.ideal R S).cotangent_ideal`

Equations
def kaehler_differential.End_equiv_aux_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
{f // = S S {f //

(Implementation) An `equiv` version of `kaehler_differential.End_equiv_aux`. Used in `kaehler_differential.End_equiv`.

Equations
noncomputable def kaehler_differential.End_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
Ω[SR] {f //

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] [ S] :
(S →₀ 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
theorem kaehler_differential.ker_total_mkq_single_add (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x y z : S) :
.mkq) (finsupp.single (x + y) z) = .mkq) z) + .mkq) z)
theorem kaehler_differential.ker_total_mkq_single_mul (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x y z : S) :
.mkq) (finsupp.single (x * y) z) = .mkq) (z * x)) + .mkq) (z * y))
theorem kaehler_differential.ker_total_mkq_single_algebra_map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : R) (y : S) :
.mkq) (finsupp.single ( S) x) y) = 0
theorem kaehler_differential.ker_total_mkq_single_algebra_map_one (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : S) :
.mkq) x) = 0
theorem kaehler_differential.ker_total_mkq_single_smul (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (r : R) (x y : S) :
.mkq) (finsupp.single (r x) y) = r .mkq) y)
noncomputable def kaehler_differential.derivation_quot_ker_total (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S ((S →₀ S)

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

Equations
theorem kaehler_differential.derivation_quot_ker_total_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : S) :
= .mkq) 1)
theorem kaehler_differential.ker_total_eq (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[simp]
theorem kaehler_differential.quot_ker_total_equiv_symm_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (ᾰ : Ω[SR]) :
@[simp]
theorem kaehler_differential.quot_ker_total_equiv_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (ᾰ : (S →₀ S) ) :
= Ω[SR] S S)) _).to_fun
noncomputable def kaehler_differential.quot_ker_total_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :

`Ω[S⁄R]` is isomorphic to `S` copies of `S` with kernel `kaehler_differential.ker_total`.

Equations
theorem kaehler_differential.ker_total_map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] (h : function.surjective B)) :
submodule.map B))) (set.range (λ (x : S), finsupp.single ( B) x) 1)) =
def derivation.comp_algebra_map {R : Type u_1} [comm_ring R] {M : Type u_3} [ M] (A : Type u_4) {B : Type u_5} [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ M] [ M] [ M] (d : B M) :
A 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] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] :

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

Equations
theorem kaehler_differential.map_comp_der (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] :
A B).comp_der) =
theorem kaehler_differential.map_D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] (x : A) :
A B) ( x) = ( B) x)
theorem kaehler_differential.map_surjective_of_surjective (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] (h : function.surjective B)) :
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] [ A] [ B] [ B] [ 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] [ A] [ B] [ B] [ B] (x : B) (y : Ω[AR]) :
(x ⊗ₜ[A] y) = x A B) y