Documentation

Mathlib.RingTheory.Derivation.Basic

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 #

See RingTheory.Derivation.Lie for

and RingTheory.Derivation.ToSquareZero for

Future project #

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)

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
    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 => AM

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

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

    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] :
    @[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
    @[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
    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
    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)
    @[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
    @[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
    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
    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] :
    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)
    @[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
    @[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
    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
    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 →+ AM

    coe_fn as an AddMonoidHom.

    Instances For
      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)
      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) :

      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
        @[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
        @[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)
        @[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
        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] :

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

        Instances For
          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) :

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

          Instances For
            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) :

            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
              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) :

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

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