PhyslibAlpha.CondensedMatter.SpinLattice.ClassicalSpins

For finite sets $\alpha$ and $\beta$ and a map $\phi: \alpha \to \beta$, `pullbackChan φ` is the unital positive linear map (representing a physical channel) from the space of observables on $\beta$ to the space of observables on $\alpha$. It maps an observable $f: \beta \to \mathbb{R}$ to its pullback along $\phi$, defined by the composition $f \circ \phi$.

Let $\alpha$ and $\beta$ be finite sets, and let $\phi: \alpha \to \beta$ be a function. For any observable $f$ in the finite classical system over $\beta$ (modeled as a real-valued function) and any element $a \in \alpha$, the application of the pullback channel $\text{pullbackChan}(\phi)$ to $f$ evaluated at $a$ is equal to $f(\phi(a))$.

Let $\alpha, \beta$, and $\gamma$ be finite sets. For any maps $\phi: \alpha \to \beta$ and $\psi: \beta \to \gamma$, let $\text{pullbackChan } \phi$ and $\text{pullbackChan } \psi$ denote the pullback channels (unital positive linear maps) that act on observables by pre-composition with $\phi$ and $\psi$ respectively. The composition of these channels satisfies $$(\text{pullbackChan } \phi) \circ (\text{pullbackChan } \psi) = \text{pullbackChan } (\psi \circ \phi),$$ where the right-hand side is the pullback channel along the composite map $\psi \circ \phi: \alpha \to \gamma$.

Given a lattice $S$ and a set of possible spin states $\sigma$, the space of classical observables for a finite region $X \subseteq S$ is the set of real-valued functions $f: \sigma^X \to \mathbb{R}$ defined on the configuration space of that region. Here, $\sigma^X$ denotes the set of all possible configurations $c: X \to \sigma$ that assign a spin state to each site in $X$.

Given two finite subsets $X$ and $Y$ of a lattice $S$ such that $X \subseteq Y$, and a spin configuration $c: Y \to \sigma$ that assigns a state in $\sigma$ to each site in $Y$, this function returns the restriction of the configuration $c$ to the subregion $X$, denoted by $c|_X: X \to \sigma$.

The net of local classical observables on a lattice $S$ with spin states $\sigma$ is a structure that assigns to each finite subset of sites $X \subseteq S$ the space of observables $\text{Obs}(X) = \{f: \sigma^X \to \mathbb{R}\}$. For any inclusion of finite sets $X \subseteq Y$, the net provides a map between the corresponding spaces of observables $\iota_{XY}: \text{Obs}(X) \to \text{Obs}(Y)$. This map is defined as the pullback along the restriction map $\text{res}_{Y \to X}: \sigma^Y \to \sigma^X$, such that for any observable $f \in \text{Obs}(X)$ and any configuration $c \in \sigma^Y$, the value of the extended observable is $(\iota_{XY} f)(c) = f(c|_X)$, where $c|_X$ denotes the restriction of the configuration $c$ to the subset $X$.

Let $S$ be a lattice and $\sigma$ be a set of spin states. If $\sigma$ is inhabited (i.e., there exists at least one spin state), then the net of local observables on $S$ is faithful. This means that for any finite subsets $X, Y \subseteq S$ such that $X \subseteq Y$, the inclusion map $\iota_{XY} : \text{Obs}(X) \to \text{Obs}(Y)$ is an order embedding. Specifically, for any two observables $f, g \in \text{Obs}(X)$, the pointwise inequality $f \le g$ holds if and only if their extensions to the larger region satisfy $\iota_{XY}(f) \le \iota_{XY}(g)$.

Let $S$ be a lattice and $G$ be a group acting on $S$. For any finite set of sites $X \subseteq S$ and any group element $g \in G$, let $g \cdot X$ denote the image of $X$ under the action of $g$. Let $\sigma$ represent the set of possible spin values at each site. This definition establishes an equivalence (bijection) between the set of spin configurations on the translated region $g \cdot X$ (functions from $g \cdot X$ to $\sigma$) and the set of spin configurations on the original region $X$ (functions from $X$ to $\sigma$). Given a configuration $c: g \cdot X \to \sigma$, the equivalence maps it to a configuration on $X$ by assigning to each $x \in X$ the value $c(g \cdot x)$.

Given a lattice $S$ and a group $G$ acting on it, let $\sigma$ be the set of spin values. For a finite region $X \subseteq S$, let $Obs(X)$ be the space of real-valued observables, which are functions from the configuration space $\sigma^X$ to $\mathbb{R}$. For any $g \in G$, $\tau_g$ is the isomorphism of order unit spaces between $Obs(X)$ and $Obs(g \cdot X)$ induced by the action of $g$. For an observable $f \in Obs(X)$, its image $\tau_g(f) \in Obs(g \cdot X)$ is defined by $(\tau_g f)(c) = f(c \circ g)$ for any configuration $c: g \cdot X \to \sigma$, where $c \circ g$ is the configuration on $X$ given by $(c \circ g)(x) = c(g \cdot x)$.

Let $S$ be a lattice and $\sigma$ be a set of spin states. For any finite regions $X, Y \subseteq S$ such that $X = Y$, let $e: X = Y$ be the proof of their equality. Let $\text{Obs}(X)$ and $\text{Obs}(Y)$ be the spaces of real-valued observables (functions from the configuration spaces $\sigma^X$ and $\sigma^Y$ to $\mathbb{R}$, respectively). The order-unit isomorphism $\text{eqIso}_e: \text{Obs}(X) \cong \text{Obs}(Y)$ identifies an observable $f \in \text{Obs}(X)$ with an observable in $\text{Obs}(Y)$. For any configuration $c: Y \to \sigma$, the value of the identified observable is given by $$(\text{eqIso}_e f)(c) = f(c \circ \text{id}_{XY})$$ where $c \circ \text{id}_{XY}$ is the configuration on $X$ obtained by identifying the elements of $X$ and $Y$ via the equality $e$.

For a group $G$ acting on a lattice $S$ with spin states $\sigma$, the `netAction` is the covariant group action of $G$ on the net of local observables $\mathcal{A}$. It assigns to each $g \in G$ a family of isomorphisms $\tau_g: \text{Obs}(X) \cong \text{Obs}(g \cdot X)$ for all finite regions $X \subseteq S$. For an observable $f \in \text{Obs}(X)$, the action is defined by $(\tau_g f)(c) = f(c \circ g)$ for any configuration $c: g \cdot X \to \sigma$, where $(c \circ g)(x) = c(g \cdot x)$. This action is compatible with the inclusion maps $\iota_{XY}: \text{Obs}(X) \to \text{Obs}(Y)$ of the net, satisfying $\tau_g \circ \iota_{XY} = \iota_{gX, gY} \circ \tau_g$, as well as the group action axioms $\tau_e = \text{id}$ and $\tau_{gh} = \tau_g \circ \tau_h$.

Let $S$ be a lattice with an inhabited set of spin states $\sigma$. Let $\mathcal{A}$ be the global system of observables, defined as the algebraic direct limit $\varinjlim \text{Obs}(X)$ of the spaces of classical observables on finite regions $X \subseteq S$. Suppose a group $G$ acts on the lattice, inducing a net action on the local observables and a corresponding group homomorphism $\beta : G \to \text{Symmetry}(\mathcal{A})$ on the global system. For any global state $\omega$ on $\mathcal{A}$, let $\{\omega_X\}_{X \subseteq S}$ be the associated compatible family of local states. Then, the family of local states is invariant under the symmetry action of $G$ if and only if the global state $\omega$ is invariant under the global symmetry action, meaning $\omega \circ \beta_g = \omega$ for all $g \in G$.