PhyslibAlpha.AlgebraicFramework.OrderUnit.Symmetry

A unital positive linear map (also called a channel) $\phi : E \to E$ is an order-automorphism if there exists another unital positive linear map $\psi : E \to E$ such that $\psi \circ \phi = \text{id}_E$ and $\phi \circ \psi = \text{id}_E$. This implies that $\phi$ is a reversible transformation where both the map and its inverse preserve the order and the unit of the space $E$.

The identity map $\text{id}_E: E \to E$ is an order-automorphism.

Given a unital positive linear map $\phi : E \to E$ (also referred to as a channel) and a proof $h$ that $\phi$ is an order-automorphism, this definition provides the inverse unital positive linear map $\phi^{-1} : E \to E$. This inverse map satisfies the conditions $\phi^{-1} \circ \phi = \text{id}_E$ and $\phi \circ \phi^{-1} = \text{id}_E$, ensuring that the reversal of the transformation is itself a valid channel (i.e., it preserves both the order and the unit of the space $E$).

Let $\phi : E \to E$ be a unital positive linear map that is an order-automorphism, and let $\phi^{-1}$ be its inverse. Then the composition of $\phi^{-1}$ and $\phi$ is the identity map on $E$, written as $\phi^{-1} \circ \phi = \text{id}_E$.

Let $E$ be a space and $\phi : E \to E$ be a unital positive linear map (a channel). If $\phi$ is an order-automorphism, let $\phi^{-1}$ denote its inverse unital positive linear map. Then the composition of $\phi$ with its inverse is the identity map on $E$, denoted as $\phi \circ \phi^{-1} = \text{id}_E$.

Let $\phi : E \to E$ be a unital positive linear map (a channel) on an order-unit space $E$. If $\phi$ is an order-automorphism with inverse $\phi^{-1}$, then for any $x \in E$, applying $\phi$ followed by $\phi^{-1}$ returns the original element: $$\phi^{-1}(\phi(x)) = x$$

Let $\phi: E \to E$ be an order-automorphism (a unital positive linear map with a unital positive linear inverse $\phi^{-1}$). For any element $x \in E$, applying the inverse map followed by the map $\phi$ returns the original element: $$\phi(\phi^{-1}(x)) = x$$

Let $E$ be an order-unit space and $\phi : E \to E$ be a unital positive linear map. If $\phi$ is an order-automorphism, then its inverse $\phi^{-1}$ is also an order-automorphism.

Let $E$ be a space and $\phi, \psi: E \to E$ be unital positive linear maps (channels). If $\phi$ and $\psi$ are order-automorphisms, then their composition $\phi \circ \psi$ is also an order-automorphism.

Let $E$ be an order-unit space (a real ordered vector space with a distinguished unit element) and let $\phi : E \to E$ be a unital positive linear map. If $\phi$ is an order-automorphism, then $\phi$ is a bijective function.

Let $E$ be a real vector space equipped with a partial order and a unit element $1$. The type `Symmetry E` is the set of all unital positive linear maps $\phi: E \to E$ (also known as channels) that are order-automorphisms. A map $\phi$ is an order-automorphism if there exists an inverse unital positive linear map $\phi^{-1}$ such that $\phi \circ \phi^{-1} = \text{id}_E$ and $\phi^{-1} \circ \phi = \text{id}_E$. This structure bundles the map with the proof that it and its inverse preserve both the ordering and the unit of $E$.

Let $E$ be a real vector space equipped with a partial order and a unit element. If $\phi$ and $\psi$ are symmetries of $E$ (unital positive linear maps that are order-automorphisms) such that $\phi(x) = \psi(x)$ holds for every $x \in E$, then $\phi = \psi$.

The identity element $1$ for the group of symmetries $\text{Symmetry } E$ is defined as the identity unital positive linear map $\text{id}_E : E \to E$.

Given two symmetries $\phi, \psi \in \text{Symmetry } E$ of a real ordered vector space with unit $E$, their multiplication $\phi \cdot \psi$ is defined as the composition of the underlying unital positive linear maps $\phi \circ \psi$. This composition results in a new order-automorphism of $E$.

This definition provides the inverse operation for the group of symmetries of $E$. For any symmetry $\phi \in \text{Symmetry } E$, its inverse $\phi^{-1}$ is the symmetry whose underlying map is the inverse unital positive linear map (channel) satisfying $\phi \circ \phi^{-1} = \text{id}_E$ and $\phi^{-1} \circ \phi = \text{id}_E$.

Let $E$ be a real ordered vector space with unit. The underlying unital positive linear map of the identity element $1$ in the group of symmetries $\text{Symmetry } E$ is the identity map $\text{id}_E$ on $E$.

Let $E$ be a real ordered vector space with a unit. For any two symmetries $\phi, \psi \in \text{Symmetry } E$, the underlying unital positive linear map (channel) of their product $\phi \cdot \psi$ in the symmetry group is equal to the composition $\phi \circ \psi$ of their individual underlying maps.

Let $E$ be a real vector space equipped with a partial order and a unit element. For any symmetry $\phi \in \text{Symmetry } E$, the underlying unital positive linear map (channel) of the inverse symmetry $\phi^{-1}$ is equal to the inverse channel of $\phi$.

The set of order-automorphisms $\text{Symmetry } E$ of a real ordered vector space $E$ with unit element $1$ forms a group. In this group, the multiplication of two symmetries $\phi$ and $\psi$ is defined as their composition $\phi \circ \psi$, the identity element is the identity map $\text{id}_E$, and the inverse of a symmetry $\phi$ is its inverse order-automorphism $\phi^{-1}$.

For a real ordered vector space with unit $E$, there is a group isomorphism between the group of symmetries $\text{Symmetry } E$ and the group of units $(E \to_{p1} [ℝ] E)^\times$ of the monoid of unital positive linear maps (channels) on $E$. This equivalence maps each symmetry $\phi$ to the unit whose underlying value is the channel $\phi$ and whose inverse is the channel $\phi^{-1}$.

The group of symmetries $\text{Symmetry } E$ acts on the state space $\mathcal{S}(E)$ (denoted as $\mathcal{S}[\mathbb{R}, E]$). For a symmetry $\phi \in \text{Symmetry } E$ and a state $\omega \in \mathcal{S}(E)$, the action is defined by $\phi \cdot \omega = \omega \circ \phi^{-1}$, where $\phi^{-1}$ is the inverse order-automorphism. This corresponds to the Schrödinger-picture pushforward of a state, where the state is transported by pulling it back along the inverse of the symmetry transformation.

Let $E$ be a real ordered vector space with a unit element. For any symmetry $\phi \in \text{Symmetry } E$ and any state $\omega \in \mathcal{S}(E)$, the group action of $\phi$ on $\omega$ is defined by the composition $\phi \cdot \omega = \omega \circ \phi^{-1}$, where $\phi^{-1}$ is the inverse order-automorphism of $\phi$.

Let $G$ be a group and $E$ be a real ordered vector space with a unit element. Given a group homomorphism $\rho : G \to \text{Symmetry } E$ that represents $G$ as a group of order-automorphisms of $E$, the function `stateSMul` defines an action of $G$ on the state space $\mathcal{S}(E)$. For any element $g \in G$ and state $\omega \in \mathcal{S}(E)$, the action results in a new state given by $g \cdot \omega = \rho(g) \cdot \omega$. Following the definition of symmetry actions on states, this is equivalent to the composition $\omega \circ (\rho(g))^{-1}$.

Let $G$ be a group and $E$ be a real ordered vector space with a unit element. For any group homomorphism $\rho : G \to \text{Symmetry } E$ and any state $\omega \in \mathcal{S}(E)$, the action of the identity element $1 \in G$ on the state $\omega$ satisfies: $$\text{stateSMul } \rho \, 1 \, \omega = \omega$$ where $\text{stateSMul}$ denotes the group action of $G$ on the state space $\mathcal{S}(E)$ induced by $\rho$.

Let $G$ be a group and $E$ be a real ordered vector space with a unit element. Let $\rho : G \to \text{Symmetry } E$ be a group homomorphism that represents $G$ as a group of order-automorphisms of $E$. For any elements $g, h \in G$ and any state $\omega \in \mathcal{S}(E)$, the action of the group on the state space satisfies the property $(gh) \cdot \omega = g \cdot (h \cdot \omega)$, where the action $g \cdot \omega$ is defined by `stateSMul ρ g ω`.

This instance defines a coercion from the type of one-parameter automorphism groups `OneParameterAutomorphismGroup E` to a function type. It allows an element $\alpha$ representing a one-parameter family of symmetries to be treated as a mapping that takes a real number $t \in \mathbb{R}$ and returns a unital positive linear map (channel) $\alpha(t) : E \to_{p1}[\mathbb{R}] E$.

For any one-parameter automorphism group $\alpha$ on a system $E$, the transformation corresponding to the parameter $0$ is the identity map on $E$, denoted as $\alpha(0) = \text{id}_E$.

Let $E$ be a system (represented as an order-unit space or effect algebra) and let $\alpha$ be a one-parameter automorphism group on $E$. For any real numbers $s$ and $t$, the automorphism associated with the sum $s + t$ is the composition of the automorphisms associated with $s$ and $t$: $$\alpha(s + t) = \alpha(s) \circ \alpha(t)$$

Given a one-parameter automorphism group $\alpha$ on a space $E$ (such as an effect algebra or order-unit space), for every $t \in \mathbb{R}$, the map $\alpha(t)$ is an order-automorphism. This means $\alpha(t)$ is a unital positive linear map with a two-sided inverse that is also a unital positive linear map. Specifically, the inverse of $\alpha(t)$ is given by $\alpha(-t)$, representing the physical intuition that running time backwards undoes the transformation.

Let $E$ be a real ordered vector space with a unit element. A one-parameter automorphism group $\alpha$ on $E$ is organized into a group homomorphism from the additive group of real numbers $(\mathbb{R}, +)$ (represented as `Multiplicative ℝ`) to the group of symmetries $\text{Symmetry } E$. This map associates each $t \in \mathbb{R}$ with the order-automorphism $\alpha(t)$, satisfying $\alpha(0) = \text{id}_E$ and $\alpha(s + t) = \alpha(s) \circ \alpha(t)$. This formulation allows the dynamics to be treated as a general group action on the state space of the system.

Let $E$ be a real ordered vector space with a unit element, and let $\mathcal{S}(E)$ denote its state space (the set of unital positive linear maps from $E$ to $\mathbb{R}$). Given a one-parameter automorphism group $\alpha$ on $E$ and an initial state $\omega \in \mathcal{S}(E)$, the function `stateEvolution` defines the state at time $t \in \mathbb{R}$. It is calculated as the action of the symmetry $\alpha(t)$ on the state $\omega$, which is equivalent to the precomposition $\omega \circ \alpha(-t)$. This evolution satisfies the group action properties: $\alpha.\text{stateEvolution}(0, \omega) = \omega$ and $\alpha.\text{stateEvolution}(s + t, \omega) = \alpha.\text{stateEvolution}(s, \alpha.\text{stateEvolution}(t, \omega))$.

Let $E$ be a real ordered vector space with a unit element, and let $\mathcal{S}(E)$ be its state space. For any one-parameter automorphism group $\alpha$ on $E$ and any initial state $\omega \in \mathcal{S}(E)$, the state evolution at time $t = 0$ is the identity, such that $\alpha.\text{stateEvolution}(0, \omega) = \omega$.

Let $E$ be a real ordered vector space with a unit element, and let $\mathcal{S}(E)$ denote its state space (the set of unital positive linear maps from $E$ to $\mathbb{R}$). For any one-parameter automorphism group $\alpha$ on $E$, any initial state $\omega \in \mathcal{S}(E)$, and any time parameters $s, t \in \mathbb{R}$, the state evolution satisfies the group property: $$\alpha.\text{stateEvolution}(s + t, \omega) = \alpha.\text{stateEvolution}(s, \alpha.\text{stateEvolution}(t, \omega))$$