PhyslibAlpha.ProbabilisticTheory.Dynamics.GeneratorIsDerivation

Generators of automorphism groups are derivations

i. Overview

If a one-parameter family `α` with `α 0 = id` preserves a bounded bilinear multiplication at every time, its generator is a derivation of that multiplication. Differentiating `α t (a b) = α t a α t b` at `0` with the product rule gives `D (a b) = D a b + a D b`. Only boundedness and bilinearity of the product are used.

ii. Key results

- `IsGenerator.isDerivation_of_isAutomorphismFamily` : the generator of a family of automorphisms is a derivation.

iii. Table of contents

A. The generator is a derivation

A. The generator is a derivation

1 declaration

theorem

The generator of a family of automorphisms is a derivation

#isDerivation_of_isAutomorphismFamily

Let $E$ be a real vector space equipped with a bounded bilinear multiplication denoted by $(a, b) \mapsto a \cdot b$ . Let $\alpha_t: E \to E$ be a one-parameter family of maps such that $\alpha_0$ is the identity map ( $\alpha_0(a) = a$ ) and each $\alpha_t$ preserves the multiplication, i.e., $\alpha_t(a \cdot b) = \alpha_t(a) \cdot \alpha_t(b)$ for all $t \in \mathbb{R}$ and $a, b \in E$ . If $D: E \to E$ is the linear generator of the family $\alpha$ , then $D$ is a derivation with respect to the multiplication, satisfying the Leibniz rule $D(a \cdot b) = (Da) \cdot b + a \cdot (Db)$ .