Physlib

PhyslibAlpha.AlgebraicFramework.Algebra.Derivation

Derivations for an arbitrary bilinear multiplication

i. Overview

A derivation is a purely *algebraic* notion: `D(a * b) = D(a) * b + a * D(b)`. No topology, no time, no continuity, no exponential — it is meaningful for a bare `NonUnitalNonAssocRing`. This is deliberately factored out of both the Jordan layer (`JordanOrderUnit/`) and any dynamical layer (`Dynamics/`): "derivation" is an algebra-axis concept, and the fact that the *generator* of a one-parameter automorphism group happens to be a derivation (`Dynamics/GeneratorIsDerivation.lean`) is a separate, genuinely analytic bridge theorem, not a definition.

`E` here is left as general as possible: only `Add`, `Mul`, and enough linearity for `D` itself to be additive/`ℝ`-linear (`E →ₗ[ℝ] E`) are assumed. `IsCommJordan`, `NonUnitalNonAssocCommRing`, and every other structure this project puts on top of a bare multiplication are irrelevant to this file — a Jordan derivation (`D(a ∘ b) = D(a) ∘ b + a ∘ D(b)`) and an associative one are literally the same predicate, `IsDerivation`, instantiated at different `Mul E`.

ii. Key definitions and results

- `IsDerivation` - `IsDerivation.zero`, `.add`, `.neg` : derivations form an additive group (stated pointwise; the submodule structure is left for a future file if needed)

iii. Table of contents

  • A. The Leibniz rule
  • B. Closure properties

A. The Leibniz rule

B. Closure properties

5 declarations

definition

DD is a derivation if D(a⋅b)=D(a)⋅b+a⋅D(b)D(a \cdot b) = D(a) \cdot b + a \cdot D(b)

Let EE be a real vector space equipped with a multiplication operation (a,b)↦a⋅b(a, b) \mapsto a \cdot b. A linear map D:E→ED: E \to E is said to be a derivation if it satisfies the Leibniz rule: D(a⋅b)=D(a)⋅b+a⋅D(b) D(a \cdot b) = D(a) \cdot b + a \cdot D(b) for all a,b∈Ea, b \in E.

theorem

The zero map is a derivation

Let EE be a real vector space equipped with a multiplication operation. The zero linear map 0:E→E0: E \to E is a derivation.

theorem

The Sum of Two Derivations is a Derivation

Let EE be a real vector space equipped with a multiplication operation. If D1,D2:E→ED_1, D_2: E \to E are linear maps that are derivations, then their sum D1+D2D_1 + D_2 is also a derivation. (A linear map DD is a derivation if it satisfies the Leibniz rule D(a⋅b)=D(a)⋅b+a⋅D(b)D(a \cdot b) = D(a) \cdot b + a \cdot D(b) for all a,b∈Ea, b \in E.)

theorem

If DD is a derivation, then −D-D is a derivation

Let EE be a real vector space equipped with a multiplication operation (a,b)↦a⋅b(a, b) \mapsto a \cdot b. If D:E→ED: E \to E is an R\mathbb{R}-linear map that is a derivation (i.e., it satisfies the Leibniz rule D(a⋅b)=D(a)⋅b+a⋅D(b)D(a \cdot b) = D(a) \cdot b + a \cdot D(b)), then the negative linear map −D-D is also a derivation.

theorem

A scalar multiple of a derivation is a derivation

Let EE be a real vector space equipped with a multiplication operation (a,b)↦a⋅b(a, b) \mapsto a \cdot b. Suppose that scalar multiplication by elements of R\mathbb{R} is compatible with the multiplication on EE in the sense that c(a⋅b)=(ca)⋅b=a⋅(cb)c(a \cdot b) = (ca) \cdot b = a \cdot (cb) for all c∈Rc \in \mathbb{R} and a,b∈Ea, b \in E. If D:E→ED: E \to E is an R\mathbb{R}-linear map that is a derivation (i.e., it satisfies the Leibniz rule D(a⋅b)=D(a)⋅b+a⋅D(b)D(a \cdot b) = D(a) \cdot b + a \cdot D(b)), then for any scalar c∈Rc \in \mathbb{R}, the map cDc D is also a derivation.