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.

See RingTheory.Derivation.Lie for

• derivation.lie_algebra: The R-derivations from A to A form a lie algebra over R.

and RingTheory.Derivation.ToSquareZero for

• 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.

Future project

• Generalize derivations into bimodules.

structure Derivation (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] extends LinearMap : 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.

• toFun : A → M
• map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (r : R) (x : A), self.toFun (r • x) = (RingHom.id R) r • self.toFun x
• map_one_eq_zero' : ↑self 1 = 0
• leibniz' : ∀ (a b : A), ↑self (a * b) = a • ↑self b + b • ↑self a

instance Derivation.instFunLikeDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : FunLike (Derivation R A M) A M

Equations

• Derivation.instFunLikeDerivation = { coe := fun (D : Derivation R A M) => D.toFun, coe_injective' := ⋯ }

instance Derivation.instAddMonoidHomClassDerivationToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToAddZeroClassToAddMonoidInstFunLikeDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : AddMonoidHomClass (Derivation R A M) A M

Equations

• ⋯ = ⋯

theorem Derivation.toFun_eq_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) : D.toFun = ⇑D

def Derivation.Simps.apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) : A → M

See Note [custom simps projection]

Equations

• Derivation.Simps.apply D = ⇑D

instance Derivation.hasCoeToLinearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Coe (Derivation R A M) (A →ₗ[R] M)

Equations

• Derivation.hasCoeToLinearMap = { coe := fun (D : Derivation R A M) => ↑D }

@[simp]

theorem Derivation.mk_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [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) : ⇑{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ } = ⇑f

@[simp]

theorem Derivation.coeFn_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (f : Derivation R A M) : ⇑↑f = ⇑f

theorem Derivation.coe_injective {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Function.Injective DFunLike.coe

theorem Derivation.ext {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (H : ∀ (a : A), D1 a = D2 a) : D1 = D2

theorem Derivation.congr_fun {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (h : D1 = D2) (a : A) : D1 a = D2 a

theorem Derivation.map_add {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) : D (a + b) = D a + D b

theorem Derivation.map_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) : D 0 = 0

@[simp]

theorem Derivation.map_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [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} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) : D (a * b) = a • D b + b • D a

theorem Derivation.map_sum {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {ι : Type u_5} (s : Finset ι) (f : ι → A) : D (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => D (f i)

@[simp]

theorem Derivation.map_smul_of_tower {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [SMul S A] [SMul S M] [LinearMap.CompatibleSMul 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} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) : D 1 = 0

@[simp]

theorem Derivation.map_algebraMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (r : R) : D ((algebraMap R A) r) = 0

@[simp]

theorem Derivation.map_coe_nat {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (n : ℕ) : D ↑n = 0

@[simp]

theorem Derivation.leibniz_pow {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [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.eqOn_adjoin {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} {s : Set A} (h : Set.EqOn (⇑D1) (⇑D2) s) : Set.EqOn ⇑D1 ⇑D2 ↑(Algebra.adjoin R s)

theorem Derivation.ext_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (s : Set A) (hs : Algebra.adjoin R s = ⊤) (h : Set.EqOn (⇑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.

instance Derivation.instZeroDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Zero (Derivation R A M)

Equations

• Derivation.instZeroDerivation = { zero := { toLinearMap := 0, map_one_eq_zero' := ⋯, leibniz' := ⋯ } }

@[simp]

theorem Derivation.coe_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : ⇑0 = 0

@[simp]

theorem Derivation.coe_zero_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : ↑0 = 0

theorem Derivation.zero_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (a : A) : 0 a = 0

instance Derivation.instAddDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Add (Derivation R A M)

Equations

• Derivation.instAddDerivation = { add := fun (D1 D2 : Derivation R A M) => { toLinearMap := ↑D1 + ↑D2, map_one_eq_zero' := ⋯, leibniz' := ⋯ } }

@[simp]

theorem Derivation.coe_add {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) : ⇑(D1 + D2) = ⇑D1 + ⇑D2

@[simp]

theorem Derivation.coe_add_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) : ↑(D1 + D2) = ↑D1 + ↑D2

theorem Derivation.add_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (a : A) : (D1 + D2) a = D1 a + D2 a

instance Derivation.instInhabitedDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Inhabited (Derivation R A M)

Equations

• Derivation.instInhabitedDerivation = { default := 0 }

instance Derivation.instSMulDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] : SMul S (Derivation R A M)

Equations

• Derivation.instSMulDerivation = { smul := fun (r : S) (D : Derivation R A M) => { toLinearMap := r • ↑D, map_one_eq_zero' := ⋯, leibniz' := ⋯ } }

@[simp]

theorem Derivation.coe_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] (r : S) (D : Derivation R A M) : ⇑(r • D) = r • ⇑D

@[simp]

theorem Derivation.coe_smul_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] (r : S) (D : Derivation R A M) : ↑(r • D) = r • ↑D

theorem Derivation.smul_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (a : A) {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] (r : S) (D : Derivation R A M) : (r • D) a = r • D a

instance Derivation.instAddCommMonoidDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : AddCommMonoid (Derivation R A M)

Equations

• Derivation.instAddCommMonoidDerivation = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

def Derivation.coeFnAddMonoidHom {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] : Derivation R A M →+ A → M

coe_fn as an AddMonoidHom.

Equations

• Derivation.coeFnAddMonoidHom = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }

instance Derivation.instDistribMulActionDerivationToAddMonoidInstAddCommMonoidDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] : DistribMulAction S (Derivation R A M)

Equations

• Derivation.instDistribMulActionDerivationToAddMonoidInstAddCommMonoidDerivation = Function.Injective.distribMulAction Derivation.coeFnAddMonoidHom ⋯ ⋯

instance Derivation.instIsCentralScalarDerivationInstSMulDerivationMulOppositeMonoidOp_rightToSMulToZeroToAddMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToSMulToSMulZeroClassToAddZeroClassToDistribSMulOp_leftToSMulToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZero {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] [DistribMulAction Sᵐᵒᵖ M] [IsCentralScalar S M] : IsCentralScalar S (Derivation R A M)

Equations

• ⋯ = ⋯

instance Derivation.instIsScalarTowerDerivationInstSMulDerivationInstSMulDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} {T : Type u_6} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [SMulCommClass T A M] [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (Derivation R A M)

Equations

• ⋯ = ⋯

instance Derivation.instSMulCommClassDerivationInstSMulDerivationInstSMulDerivation {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} {T : Type u_6} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulCommClass S A M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [SMulCommClass T A M] [SMulCommClass S T M] : SMulCommClass S T (Derivation R A M)

Equations

• ⋯ = ⋯

instance Derivation.instModule {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [Semiring S] [Module S M] [SMulCommClass R S M] [SMulCommClass S A M] : Module S (Derivation R A M)

Equations

• Derivation.instModule = Function.Injective.module S Derivation.coeFnAddMonoidHom ⋯ ⋯

def LinearMap.compDer {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Derivation.coe_to_linearMap_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) : ↑((LinearMap.compDer f) D) = ↑R f ∘ₗ ↑D

@[simp]

theorem Derivation.coe_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) : ⇑((LinearMap.compDer f) D) = ⇑(↑R f ∘ₗ ↑D)

@[simp]

theorem Derivation.llcomp_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) : Derivation.llcomp f = LinearMap.compDer f

def Derivation.llcomp {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower 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

Equations

• Derivation.llcomp = { toAddHom := { toFun := fun (f : M →ₗ[A] N) => LinearMap.compDer f, map_add' := ⋯ }, map_smul' := ⋯ }

def LinearEquiv.compDer {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower R A N] (e : M ≃ₗ[A] N) : Derivation R A M ≃ₗ[R] Derivation R A N

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

Equations

• LinearEquiv.compDer e = let __src := LinearMap.compDer ↑e; { toLinearMap := __src, invFun := ⇑(LinearMap.compDer ↑(LinearEquiv.symm e)), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Derivation.compAlgebraMap_apply {R : Type u_1} (A : Type u_2) {B : Type u_3} {M : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [AddCommMonoid M] [Algebra R A] [Algebra R B] [Module A M] [Module B M] [Module R M] [Algebra A B] [IsScalarTower R A B] [IsScalarTower A B M] (d : Derivation R B M) : ∀ (a : A), (Derivation.compAlgebraMap A d) a = d ((algebraMap A B) a)

def Derivation.compAlgebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} {M : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [AddCommMonoid M] [Algebra R A] [Algebra R B] [Module A M] [Module B M] [Module R M] [Algebra A B] [IsScalarTower R A B] [IsScalarTower A B M] (d : Derivation R B M) : Derivation R 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

• Derivation.compAlgebraMap A d = { toLinearMap := LinearMap.comp (↑d) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)), map_one_eq_zero' := ⋯, leibniz' := ⋯ }

def Derivation.restrictScalars (R : Type u_1) {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [CommSemiring S] [Algebra S A] [Module S M] [LinearMap.CompatibleSMul A M R S] (d : Derivation S A M) : Derivation R 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

• Derivation.restrictScalars R d = { toLinearMap := ↑R ↑d, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

def Derivation.mk' {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCancelCommMonoid 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 = { toLinearMap := D, map_one_eq_zero' := ⋯, leibniz' := h }

@[simp]

theorem Derivation.coe_mk' {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCancelCommMonoid 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'_linearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCancelCommMonoid 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

theorem Derivation.map_neg {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) (a : A) : D (-a) = -D a

theorem Derivation.map_sub {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) : D (a - b) = D a - D b

@[simp]

theorem Derivation.map_coe_int {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup 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} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) {a : A} {b : A} (h : a * b = 1) : D a = -a ^ 2 • D b

theorem Derivation.leibniz_invOf {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup 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} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {K : Type u_4} [Field K] [Module K M] [Algebra R K] (D : Derivation R K M) (a : K) : D a⁻¹ = -a⁻¹ ^ 2 • D a

instance Derivation.instNegDerivationToCommSemiringToCommSemiringToAddCommMonoid {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] : Neg (Derivation R A M)

Equations

• Derivation.instNegDerivationToCommSemiringToCommSemiringToAddCommMonoid = { neg := fun (D : Derivation R A M) => Derivation.mk' (-↑D) ⋯ }

@[simp]

theorem Derivation.coe_neg {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) : ⇑(-D) = -⇑D

@[simp]

theorem Derivation.coe_neg_linearMap {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) : ↑(-D) = -↑D

theorem Derivation.neg_apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D : Derivation R A M) (a : A) : (-D) a = -D a

instance Derivation.instSubDerivationToCommSemiringToCommSemiringToAddCommMonoid {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] : Sub (Derivation R A M)

Equations

• Derivation.instSubDerivationToCommSemiringToCommSemiringToAddCommMonoid = { sub := fun (D1 D2 : Derivation R A M) => Derivation.mk' (↑D1 - ↑D2) ⋯ }

@[simp]

theorem Derivation.coe_sub {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) : ⇑(D1 - D2) = ⇑D1 - ⇑D2

@[simp]

theorem Derivation.coe_sub_linearMap {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) : ↑(D1 - D2) = ↑D1 - ↑D2

theorem Derivation.sub_apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (a : A) : (D1 - D2) a = D1 a - D2 a

instance Derivation.instAddCommGroupDerivationToCommSemiringToCommSemiringToAddCommMonoid {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] : AddCommGroup (Derivation R A M)

Equations

• Derivation.instAddCommGroupDerivationToCommSemiringToCommSemiringToAddCommMonoid = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯