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 fromAtoM. This has anA-module structure.derivation.llcomp: We may compose linear maps and derivations to obtain a derivation, and the composition is bilinear.derivation.lie_algebra: TheR-derivations fromAtoAform an lie algebra overR.derivation_to_square_zero_equiv_lift: TheR-derivations fromAinto a square-zero idealIofBcorresponds to the liftsA →ₐ[R] Bof the mapA →ₐ[R] B ⧸ I.kaehler_differential: The module of kaehler differentials. For anR-algebraS, we provide the notationΩ[S⁄R]forkaehler_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 ofDspansΩ[S⁄R]as anS-module.kaehler_differential.linear_map_equiv_derivation: The isomorphismHom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M).
Future project #
Generalize this into bimodules.
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)
- to_linear_map : A →ₗ[R] M
- map_one_eq_zero' : ⇑(self.to_linear_map) 1 = 0
- leibniz' : ∀ (a b : A), ⇑(self.to_linear_map) (a * b) = a • ⇑(self.to_linear_map) b + b • ⇑(self.to_linear_map) a
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
- derivation.has_smul
- derivation.distrib_mul_action
- derivation.module
- derivation.has_sizeof_inst
- derivation.add_monoid_hom_class
- derivation.has_coe_to_fun
- derivation.has_coe_to_linear_map
- derivation.has_zero
- derivation.has_add
- derivation.inhabited
- derivation.add_comm_monoid
- derivation.is_central_scalar
- derivation.is_scalar_tower
- derivation.has_neg
- derivation.has_sub
- derivation.add_comm_group
- derivation.has_bracket
- derivation.lie_ring
- derivation.lie_algebra
- left_invariant_derivation.derivation.has_coe
@[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] :
add_monoid_hom_class (derivation R A M) A M
Equations
- derivation.add_monoid_hom_class = {coe := λ (D : derivation R A M), D.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_zero := _}
@[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
- derivation.has_coe_to_fun = {coe := λ (D : derivation R A M), D.to_linear_map.to_fun}
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) :
D.to_linear_map.to_fun = ⇑D
@[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
- derivation.has_coe_to_linear_map = {coe := λ (D : derivation R A M), D.to_linear_map}
@[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) :
D.to_linear_map = ↑D
@[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) :
⇑{to_linear_map := f, map_one_eq_zero' := h₁, leibniz' := h₂} = ⇑f
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :
@[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) :
@[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) :
@[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 : ℕ) :
@[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 : ℕ) :
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) :
set.eq_on ⇑D1 ⇑D2 ↑(algebra.adjoin R 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] :
has_zero (derivation R A M)
Equations
- derivation.has_zero = {zero := {to_linear_map := 0, map_one_eq_zero' := _, leibniz' := _}}
@[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] :
@[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] :
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) :
@[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] :
has_add (derivation R A M)
Equations
- derivation.has_add = {add := λ (D1 D2 : derivation R A M), {to_linear_map := ↑D1 + ↑D2, map_one_eq_zero' := _, leibniz' := _}}
@[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) :
@[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) :
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) :
@[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] :
inhabited (derivation R A M)
Equations
- derivation.inhabited = {default := 0}
@[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] :
has_smul S (derivation R A M)
Equations
- derivation.has_smul = {smul := λ (r : S) (D : derivation R A M), {to_linear_map := r • ↑D, map_one_eq_zero' := _, leibniz' := _}}
@[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) :
@[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) :
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) :
@[protected, 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_comm_monoid M]
[module A M]
[module R M] :
add_comm_monoid (derivation R A M)
Equations
- derivation.add_comm_monoid = function.injective.add_comm_monoid coe_fn derivation.coe_injective derivation.coe_zero derivation.coe_add derivation.add_comm_monoid._proof_3
def
derivation.coe_fn_add_monoid_hom
{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] :
derivation R A M →+ A → M
coe_fn as an add_monoid_hom.
Equations
- derivation.coe_fn_add_monoid_hom = {to_fun := coe_fn derivation.has_coe_to_fun, map_zero' := _, map_add' := _}
@[protected, instance]
def
derivation.distrib_mul_action
{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] :
distrib_mul_action S (derivation R A M)
@[protected, instance]
def
derivation.is_central_scalar
{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]
[distrib_mul_action Sᵐᵒᵖ M]
[is_central_scalar S M] :
is_central_scalar S (derivation R A M)
@[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
- derivation.module = function.injective.module S derivation.coe_fn_add_monoid_hom derivation.coe_injective derivation.module._proof_1
@[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] :
is_scalar_tower R A (derivation 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) :
derivation R A M →ₗ[R] derivation 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
- f.comp_der = {to_fun := λ (D : derivation R A M), {to_linear_map := ↑f.comp ↑D, map_one_eq_zero' := _, leibniz' := _}, map_add' := _, map_smul' := _}
@[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] :
(M →ₗ[A] N) →ₗ[A] derivation R A M →ₗ[R] derivation R A N
The composition of a derivation with a linear map as a bilinear map
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) :
derivation R A M
Define derivation R A M from a linear map when M is cancellative by verifying the Leibniz
rule.
Equations
- derivation.mk' D h = {to_linear_map := D, map_one_eq_zero' := _, leibniz' := h}
@[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) :
⇑(derivation.mk' D h) = ⇑D
@[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) :
↑(derivation.mk' D h) = D
@[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) :
@[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) :
@[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 : ℤ) :
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] :
@[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] :
has_neg (derivation R A M)
Equations
- derivation.has_neg = {neg := λ (D : derivation R A M), derivation.mk' (-↑D) _}
@[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) :
@[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] :
has_sub (derivation R A M)
Equations
- derivation.has_sub = {sub := λ (D1 D2 : derivation R A M), derivation.mk' (↑D1 - ↑D2) _}
@[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) :
@[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) :
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) :
@[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] :
add_comm_group (derivation R A M)
Equations
- derivation.add_comm_group = function.injective.add_comm_group coe_fn derivation.add_comm_group._proof_3 derivation.add_comm_group._proof_4 derivation.add_comm_group._proof_5 derivation.coe_neg derivation.coe_sub derivation.add_comm_group._proof_6 derivation.add_comm_group._proof_7
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] :
has_bracket (derivation R A A) (derivation R A A)
The commutator of derivations is again a derivation.
Equations
- derivation.has_bracket = {bracket := λ (D1 D2 : derivation R A A), derivation.mk' ⁅↑D1,↑D2⁆ _}
@[protected, 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 algebra.to_module, to_has_bracket := derivation.has_bracket _inst_3, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[protected, 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
- derivation.lie_algebra = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action derivation.module, add_smul := _, zero_smul := _}, lie_smul := _}
def
diff_to_ideal_of_quotient_comp_eq
{R A : Type u}
{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
- diff_to_ideal_of_quotient_comp_eq I f₁ f₂ e = linear_map.cod_restrict (submodule.restrict_scalars R I) (f₁.to_linear_map - f₂.to_linear_map) _
@[simp]
theorem
diff_to_ideal_of_quotient_comp_eq_apply
{R A : Type u}
{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) :
def
derivation_to_square_zero_of_lift
{R A : Type u}
{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)) :
derivation R 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
- derivation_to_square_zero_of_lift I hI f e = {to_linear_map := {to_fun := (diff_to_ideal_of_quotient_comp_eq I f (is_scalar_tower.to_alg_hom R A B) _).to_fun, map_add' := _, map_smul' := _}, map_one_eq_zero' := _, leibniz' := _}
theorem
derivation_to_square_zero_of_lift_apply
{R A : Type u}
{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) :
↑(⇑(derivation_to_square_zero_of_lift I hI f e) x) = ⇑f x - ⇑(algebra_map A B) x
def
lift_of_derivation_to_square_zero
{R A : Type u}
{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
- lift_of_derivation_to_square_zero I hI f = {to_fun := ((submodule.restrict_scalars R I).subtype.comp f.to_linear_map + (is_scalar_tower.to_alg_hom R A B).to_linear_map).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
lift_of_derivation_to_square_zero_apply
{R A : Type u}
{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) :
⇑(lift_of_derivation_to_square_zero I hI f) x = ↑(⇑f x) + ⇑(algebra_map A B) x
@[simp]
theorem
lift_of_derivation_to_square_zero_mk_apply
{R A : Type u}
{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) :
⇑(ideal.quotient.mk I) (⇑(lift_of_derivation_to_square_zero I hI d) x) = ⇑(algebra_map A (B ⧸ I)) x
def
derivation_to_square_zero_equiv_lift
{R A : Type u}
{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] :
derivation R A ↥I ≃ {f // (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,
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
- derivation_to_square_zero_equiv_lift I hI = {to_fun := λ (d : derivation R A ↥I), ⟨lift_of_derivation_to_square_zero I hI d, _⟩, inv_fun := λ (f : {f // (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)}), derivation_to_square_zero_of_lift I hI f.val _, left_inv := _, right_inv := _}
@[simp]
theorem
derivation_to_square_zero_equiv_lift_symm_apply
{R A : Type u}
{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 : {f // (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)}) :
⇑((derivation_to_square_zero_equiv_lift I hI).symm) f = derivation_to_square_zero_of_lift I hI f.val _
@[simp]
theorem
derivation_to_square_zero_equiv_lift_apply_coe
{R A : Type u}
{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) :
↑(⇑(derivation_to_square_zero_equiv_lift I hI) d) = lift_of_derivation_to_square_zero I hI d
@[reducible]
def
kaehler_differential.ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
ideal (tensor_product R S 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) :
tensor_product R S 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
- D.tensor_product_to = tensor_product.algebra_tensor_module.lift (⇑((linear_map.lsmul S (S →ₗ[R] M)).flip) D.to_linear_map)
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) :
theorem
derivation.tensor_product_to_mul
{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 y : tensor_product R S S) :
⇑(D.tensor_product_to) (x * y) = ⇑(algebra.tensor_product.lmul' R) x • ⇑(D.tensor_product_to) y + ⇑(algebra.tensor_product.lmul' R) y • ⇑(D.tensor_product_to) x
theorem
kaehler_differential.submodule_span_range_eq_ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
submodule.span S (set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) = submodule.restrict_scalars S (kaehler_differential.ideal R S)
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]
[algebra R S] :
ideal.span (set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) = kaehler_differential.ideal R S
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.
@[protected, instance]
def
kaehler_differential.module_3
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
module (tensor_product R S S) Ω[ S ⁄ R ]
@[protected, instance]
def
kaehler_differential.add_comm_group
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
add_comm_group Ω[ S ⁄ R ]
@[protected, instance]
def
kaehler_differential.is_scalar_tower
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
is_scalar_tower S (tensor_product R S S) Ω[ S ⁄ R ]
@[protected, instance]
def
kaehler_differential.is_scalar_tower'
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
is_scalar_tower R S Ω[ S ⁄ R ]
def
kaehler_differential.D_linear_map
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
(Implementation) The underlying linear map of the derivation into Ω[S⁄R].
Equations
- kaehler_differential.D_linear_map R S = (linear_map.restrict_scalars R (kaehler_differential.ideal R S).to_cotangent).comp (linear_map.cod_restrict (submodule.restrict_scalars R (kaehler_differential.ideal R S)) (algebra.tensor_product.include_right.to_linear_map - algebra.tensor_product.include_left.to_linear_map) _)
theorem
kaehler_differential.D_linear_map_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(s : S) :
⇑(kaehler_differential.D_linear_map R S) s = ⇑((kaehler_differential.ideal R S).to_cotangent) ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
def
kaehler_differential.D
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
derivation R S Ω[ S ⁄ R ]
The universal derivation into Ω[S⁄R].
Equations
- kaehler_differential.D R S = {to_linear_map := {to_fun := (kaehler_differential.D_linear_map R S).to_fun, map_add' := _, map_smul' := _}, map_one_eq_zero' := _, leibniz' := _}
theorem
kaehler_differential.D_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(s : S) :
⇑(kaehler_differential.D R S) s = ⇑((kaehler_differential.ideal R S).to_cotangent) ⟨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]
[algebra R S] :
submodule.span S (set.range ⇑(kaehler_differential.D R S)) = ⊤
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
theorem
derivation.lift_kaehler_differential_apply
{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 : ↥(kaehler_differential.ideal R S)) :
⇑(D.lift_kaehler_differential) (⇑((kaehler_differential.ideal R S).to_cotangent) x) = ⇑(D.tensor_product_to) ↑x
theorem
derivation.lift_kaehler_differential_comp
{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) :
⇑(D.lift_kaehler_differential.comp_der) (kaehler_differential.D R S) = D
@[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' : Ω[ S ⁄ R ] →ₗ[S] M)
(hf : ⇑(f.comp_der) (kaehler_differential.D R S) = ⇑(f'.comp_der) (kaehler_differential.D R S)) :
f = f'
theorem
derivation.lift_kaehler_differential_D
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
theorem
kaehler_differential.D_tensor_product_to
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : ↥(kaehler_differential.ideal R S)) :
⇑((kaehler_differential.D R S).tensor_product_to) ↑x = ⇑((kaehler_differential.ideal R S).to_cotangent) x
theorem
kaehler_differential.tensor_product_to_surjective
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
def
kaehler_differential.linear_map_equiv_derivation
(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] :
The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations
from S to M.
Equations
- kaehler_differential.linear_map_equiv_derivation R S = {to_fun := (⇑(derivation.llcomp.flip) (kaehler_differential.D R S)).to_fun, map_add' := _, map_smul' := _, inv_fun := derivation.lift_kaehler_differential _inst_7, left_inv := _, right_inv := _}