Physlib

PhyslibAlpha.AlgebraicFramework.Dynamics.OneParameterGroup

One-parameter groups acting on a bare carrier

i. Overview

The most primitive notion of time evolution is a group action `α : G → E → E`. This file specializes only the group to `G = (ℝ, +)` — nothing about *what `α` preserves* (linearity, order, a Jordan product, a `⋆`-structure, ...) and nothing about *continuity* belongs here. Those are independent axes:

- structure preservation is a predicate about `α t` for each fixed `t` (see e.g. `Algebra/Derivation.lean`'s companion notion for the infinitesimal picture, or state directly `∀ t a b, α t (a * b) = α t a * α t b` at the point of use — no dedicated class is introduced here since the right notion of "automorphism" depends on which structure `E` carries); - continuity, and the existence of a generator, is `Dynamics/Generator.lean`, requiring a topology `E` need not have at all to be a one-parameter group in the sense below.

This mirrors the point that an Archimedean order-unit space's topology (`OrderUnit/Norm.lean`) is not "AOU has dynamics" — it only supplies enough structure that a generic dynamical construction can later be instantiated there. Likewise here: `E` need not be an order-unit space, a Jordan algebra, or carry any topology for `IsOneParameterGroup` to be meaningful.

ii. Key definitions and results

  • `IsOneParameterGroup`

iii. Table of contents

  • A. The group law

A. The group law

3 declarations

theorem

α(−t)\alpha(-t) is the left inverse of α(t)\alpha(t) for one-parameter groups

For a one-parameter group α\alpha acting on a carrier set EE, any time t∈Rt \in \mathbb{R}, and any element a∈Ea \in E, the transformation at time −t-t acts as the left inverse of the transformation at time tt. That is, α(−t)(α(t)(a))=a\alpha(-t)(\alpha(t)(a)) = a.

theorem

Right inverse property of a one-parameter group: α(t)∘α(−t)=id\alpha(t) \circ \alpha(-t) = \text{id}

Let EE be a set and α:R→E→E\alpha : \mathbb{R} \to E \to E be a one-parameter group. For any t∈Rt \in \mathbb{R} and any a∈Ea \in E, the application of the group element α(t)\alpha(t) to α(−t)a\alpha(-t)a returns the original element, i.e., α(t)(α(−t)a)=a\alpha(t)(\alpha(-t)a) = a.

theorem

Each α(t)\alpha(t) in a one-parameter group is a bijection

Let α\alpha be a one-parameter group acting on a carrier EE. For any real number t∈Rt \in \mathbb{R}, the transformation α(t):E→E\alpha(t) : E \to E is a bijective function.