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.

source

structure Derivation (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] (M : Type u_3) [AddCommMonoid M] [Module A M] [Module R M] extends LinearMap :

Type (max u_2 u_3)

toFun : A → M
map_add' : ∀ (x y : A), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
map_smul' : ∀ (r : R) (x : A), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
map_one_eq_zero' : ↑↑s 1 = 0
leibniz' : ∀ (a b : A), ↑↑s (a * b) = a • ↑↑s b + b • ↑↑s 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

source

instance Derivation.instAddMonoidHomClassDerivationToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToAddZeroClassToAddMonoid {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

AddMonoidHomClass (Derivation R A M) A M

source

instance Derivation.instCoeFunDerivationForAll {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

CoeFun (Derivation R A M) fun x => A → M

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

source

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

D.toFun = ↑D

source

instance Derivation.hasCoeToLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

Coe (Derivation R A M) (A →ₗ[R] M)

source

@[simp]

theorem Derivation.mk_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid 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) :

↑{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ } = ↑f

source

@[simp]

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

↑↑f = ↑f

source

theorem Derivation.coe_injective {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

Function.Injective FunLike.coe

source

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

source

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

source

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

↑D (a + b) = ↑D a + ↑D b

source

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

↑D 0 = 0

source

@[simp]

theorem Derivation.map_smul {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) (r : R) (a : A) :

↑D (r • a) = r • ↑D a

source

@[simp]

theorem Derivation.leibniz {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) :

↑D (a * b) = a • ↑D b + b • ↑D a

source

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

↑D (Finset.sum s fun i => f i) = Finset.sum s fun i => ↑D (f i)

source

@[simp]

theorem Derivation.map_smul_of_tower {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] {S : Type u_4} [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

source

@[simp]

theorem Derivation.map_one_eq_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) :

↑D 1 = 0

source

@[simp]

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

↑D (↑(algebraMap R A) r) = 0

source

@[simp]

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

↑D ↑n = 0

source

@[simp]

theorem Derivation.leibniz_pow {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (n : ℕ) :

↑D (a ^ n) = n • a ^ (n - 1) • ↑D a

source

theorem Derivation.eqOn_adjoin {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [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)

source

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

source

instance Derivation.instZeroDerivation {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

Zero (Derivation R A M)

source

@[simp]

theorem Derivation.coe_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

↑0 = 0

source

@[simp]

theorem Derivation.coe_zero_linearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

↑0 = 0

source

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

↑0 a = 0

source

instance Derivation.instAddDerivation {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

Add (Derivation R A M)

source

@[simp]

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

↑(D1 + D2) = ↑D1 + ↑D2

source

@[simp]

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

↑(D1 + D2) = ↑D1 + ↑D2

source

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

source

instance Derivation.instInhabitedDerivation {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] :

Inhabited (Derivation R A M)

source

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

SMul S (Derivation R A M)

source

@[simp]

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

↑(r • D) = r • ↑D

source

@[simp]

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

↑(r • D) = r • ↑D

source

theorem Derivation.smul_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (a : A) {S : Type u_4} [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

source

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

AddCommMonoid (Derivation R A M)

source

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

Derivation R A M →+ A → M

coe_fn as an AddMonoidHom.

Instances For

source

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

DistribMulAction S (Derivation R A M)

source

instance Derivation.instIsCentralScalarDerivationInstSMulDerivationMulOppositeMonoidOp_rightToSMulToZeroToAddMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToSMulToSMulZeroClassToAddZeroClassToDistribSMulOp_leftToSMulToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZero {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] {S : Type u_4} [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)

source

instance Derivation.instIsScalarTowerDerivationInstSMulDerivationInstSMulDerivation {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] {S : Type u_4} {T : Type u_5} [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)

source

instance Derivation.instSMulCommClassDerivationInstSMulDerivationInstSMulDerivation {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] {S : Type u_4} {T : Type u_5} [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)

source

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

Module S (Derivation R A M)

source

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

Instances For

source

@[simp]

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

↑(↑(LinearMap.compDer f) D) = LinearMap.comp (↑R f) ↑D

source

@[simp]

theorem Derivation.coe_comp {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_4} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) :

↑(↑(LinearMap.compDer f) D) = ↑(LinearMap.comp (↑R f) ↑D)

source

@[simp]

theorem Derivation.llcomp_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] {N : Type u_4} [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

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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.

Instances For

source

@[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

source

@[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

source

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

source

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

source

@[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

source

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

source

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

source

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

source

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)

source

@[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

source

@[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

source

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

source

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)

source

@[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

source

@[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

source

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

source

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)