States and pullback of observables [fdip-002B]
✍️sourceAGENTDRAFTED
- October 23, 2026
States and pullback of observables [fdip-002B]
✍️sourceAGENTDRAFTED
- October 23, 2026
How can a model describe many possible fields and average what we observe? A law on a finite set of configurations assigns probability weights to those fields and averages their observables. The 16 binary fields on the four-cycle give a concrete example: summing weights over configurations with the same retained values produces the retained law. These probability weights are chosen independently of the edge energies. Real probability weights on binary fields are distinct from real-valued field coordinates. Observable algebras and normalized functionals express this operation without assuming a finite configuration set.
A supplied algebra map pulls a functional back by precomposition. Over the reals or complexes, positivity and the involution determine which functionals are states; the real dual-number example explains why the hypotheses matter. Coordinate restriction then pulls polynomial observables back. For real fields with infinitely many configurations, reference measure and Gaussian integrability give the corresponding expectations.
Definition 1. Normalized linear functionals [fdip-0021]AGENTDRAFTED
- October 23, 2026
Definition 1. Normalized linear functionals [fdip-0021]AGENTDRAFTED
- October 23, 2026
Let \(R\) be a commutative unital ring, allowing \(1=0\), and let \(A\) be a unital associative algebra over \(R\). Its scalar map is \(\eta :R\to A\), \(r\mapsto r1_A\), with central image. A normalized linear functional is an ordinary \(R\)-linear map \(\omega :A\to R\) satisfying \(\omega (1_A)=1_R\). Thus \(\omega (ra+sb)=r\omega (a)+s\omega (b)\); the coefficient map for linearity is \(\mathrm {id}_R\), not a nontrivial semilinear twist. This is a member of the dual module, with an additional normalization condition.
Normalization is equivalent to \(\omega \circ \eta =\mathrm {id}_R\). In particular, a normalized functional can exist only if \(\eta \) is injective. This necessary condition alone is not a claim of existence.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
If \(\omega (1_A)=1_R\), linearity gives \(\omega (\eta (r))=\omega (r1_A)=r\omega (1_A)=r\). Conversely, evaluating \(\omega \eta =\mathrm {id}_R\) at \(1_R\) gives \(\omega (1_A)=1_R\). A map with a left inverse is injective.
For example, the scalar map \(\mathbb Z\to \mathbb Z/2\mathbb Z\) is not injective, so this algebra admits no normalized \(\mathbb Z\)-linear functional. If \(A\) is the zero algebra, normalization is possible exactly when \(R\) is the zero ring. If \(R\) is the zero ring, every unital \(R\)-module is zero, since \(a=1_Ra=0_Ra=0\); its unique functional is normalized.
The algebra conventions are those of
[stacks2017stacks, Section 22.2], Tag 09JF and
[jadczyk2019notes, Definition 1.6, p. 4].
Mathlib's Module.Dual supplies the ordinary linear dual;
normalization and the scalar left-inverse criterion are the additional
conditions proved here. No order, involution or topology is part of this definition.
Example 2. Observables on a finite configuration set [fdip-0022]AGENTDRAFTED
- October 23, 2026
Example 2. Observables on a finite configuration set [fdip-0022]AGENTDRAFTED
- October 23, 2026
Let \(V\) be a finite vertex set and \(S\) a finite set of possible values. A configuration is a function \(\sigma :V\to S\); the configuration set is \(\Omega =S^V\). The set \(\Omega \) is distinct from the vertex set \(V\): an observable takes a whole configuration as its input. For a commutative unital ring \(R\), set \[A_\Omega =\operatorname {Map}(\Omega ,R).\] This is the pointwise function algebra: \((f+g)(\sigma )=f(\sigma )+g(\sigma )\), \((fg)(\sigma )=f(\sigma )g(\sigma )\) and \((rf)(\sigma )=rf(\sigma )\), with unit the constant function \(1_R\).
For each \(\sigma \in \Omega \), evaluation \(\operatorname {ev}_\sigma (f)=f(\sigma )\) is a unital \(R\)-algebra map and a normalized linear functional. The scalar map sends \(r\) to the constant function \(r\). The indicator \(\delta _\sigma \) is \(1_R\) at \(\sigma \) and \(0_R\) elsewhere. These are the same indicators used in counting duality for finite functions, now indexed by configurations.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Each algebra law follows by evaluating at every configuration and using the corresponding law in \(R\). Evaluation preserves addition, scalar multiplication, products and the unit by the displayed definitions. The indicators satisfy \[\delta _\sigma ^2=\delta _\sigma ,\qquad \delta _\sigma \delta _\tau =0\ (\sigma \ne \tau ),\qquad \sum _{\sigma \in \Omega }\delta _\sigma =1.\] These equalities hold pointwise, including when \(R\) is the zero ring.
If \(V=\varnothing \), then \(S^V\) contains the unique empty function, even when \(S=\varnothing \). If \(S=\varnothing \) and \(V\ne \varnothing \), then \(\Omega =\varnothing \); its function algebra is the zero algebra. There is then no evaluation at a configuration.
The underlying unital algebra convention is
[stacks2017stacks, Section 22.2], Tag 09JF.
Mathlib's Pi.algebra, Pi.evalAlgHom and
Pi.constAlgHom provide the pointwise algebra, evaluation and
constant algebra maps. The configuration interpretation and the empty-set
cases above are direct consequences of these definitions.
Proposition 3. Finite functionals and their weights [fdip-0023]AGENTDRAFTED
- October 23, 2026
Proposition 3. Finite functionals and their weights [fdip-0023]AGENTDRAFTED
- October 23, 2026
For a finite set \(\Omega \) and commutative unital ring \(R\), every \(R\)-linear functional on the function algebra has a unique weight function \(p:\Omega \to R\), given by \[\omega (f)=\sum _{x\in \Omega }p(x)f(x),\qquad p(x)=\omega (\delta _x).\] Conversely, every such weight function defines an \(R\)-linear functional. It is normalized exactly when \(\sum _xp(x)=1_R\).
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Pointwise evaluation gives \(f=\sum _x f(x)\delta _x\). Linearity therefore gives the stated formula, using commutativity of \(R\) to write the coefficients in either order. Conversely, distributivity of the finite sum proves linearity of the formula. Evaluating it on \(\delta _y\) recovers \(p(y)\), proving uniqueness in both directions. Evaluating at \(1=\sum _x\delta _x\) proves the normalization criterion.
When \(\Omega =\varnothing \), the sole functional is the zero map from the zero algebra and its total weight is \(0_R\); it is normalized exactly when \(R\) is the zero ring. When \(\Omega \ne \varnothing \), a chosen evaluation is normalized over every \(R\). Uniform weights \(p(x)=c\) on a set of size \(n>0\) are normalized exactly when \((n1_R)c=1_R\). Such normalized uniform weights exist exactly when \(n1_R\) is a unit, and then the unique coefficient is \(c=(n1_R)^{-1}\). Thus failure of uniform normalization does not imply failure of all normalized functionals.
More generally, for raw weights \(w(x)\) with total \(Z=\sum _xw(x)\), a common rescaling \(p(x)=cw(x)\) is normalized exactly when \(cZ=1_R\). This is possible exactly when \(Z\) is a unit, and then \(c=Z^{-1}\) is unique. No division by a nonunit is defined by this formula. In the zero ring the sole element is a unit, so the same criterion applies. For real nonnegative weights, \(Z>0\) exactly when at least one weight is positive; all-zero weights cannot be normalized by rescaling.
This is the indicator-basis argument of finite function duality, with the unital algebra convention of [stacks2017stacks, Section 22.2], Tag 09JF. For real nonnegative normalized weights it gives the finite expectation. No positivity or division is needed for the ring-valued classification.
Definition 4. Real and complex algebraic states [fdip-0024]AGENTDRAFTED
- October 23, 2026
Definition 4. Real and complex algebraic states [fdip-0024]AGENTDRAFTED
- October 23, 2026
Let \(K=\mathbb R\) or \(K=\mathbb C\), with conjugation the identity in the real case. Let \(A\) be a unital associative \(K\)-algebra equipped with an additive operation \(a\mapsto a^*\) satisfying \[\begin {aligned} (\lambda a)^*&=\overline \lambda a^*,& (ab)^*&=b^*a^*,\\ (a^*)^*&=a,&1^*&=1. \end {aligned}\] There is no graded sign in the product law. A \(K\)-linear functional \(\omega :A\to K\) is Hermitian positive when \[\omega (a^*)=\overline {\omega (a)},\qquad \omega (a^*a)\in \mathbb R_{\geq 0}\quad (a\in A).\] A real algebraic state, respectively a complex algebraic state, is such a functional that is also normalized. The scalar field and involution are part of the assertion.
Over \(\mathbb C\), nonnegativity on all \(a^*a\) already implies Hermiticity, without assuming normalization. Over \(\mathbb R\), Hermiticity is a separate requirement, as the real dual-number example shows.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Suppose \(K=\mathbb C\) and \(\omega (a^*a)\in \mathbb R_{\geq 0}\) for every \(a\). For \(h=h^*\), expansion and linearity give \[\begin {aligned} 4\omega (h)={}&\omega ((1+h)^*(1+h))\\ &-\omega ((1-h)^*(1-h))\in \mathbb R. \end {aligned}\] For arbitrary \(a\), put \(h=(a+a^*)/2\) and \(k=(a-a^*)/(2i)\). Conjugate scalar compatibility gives \(h=h^*\), \(k=k^*\), \(a=h+ik\) and \(a^*=h-ik\). The preceding calculation makes \(\omega (h)\) and \(\omega (k)\) real. Hence \(\omega (a^*)=\omega (h)-i\omega (k)=\overline {\omega (a)}\).
For these conventions, see [waldmann2004states, Section 3.1, p. 9; Definition 3.7 and Definition 3.9 with Remark 3.10(iv), p. 11]. Waldmann works over a complexification of an ordered ring. Here the coefficients are the ordinary fields \(\mathbb R\) and \(\mathbb C\); the real Hermiticity requirement is explicit. On p. 9, Definition 3.1 prints \(R=-P\sqcup \{0\}\sqcup R\); the intended final \(P\), rather than the printed \(R\), is a mathematical emendation, not a verbatim transcription.
The ordinary linear involution is not a substitute for conjugate scalar compatibility over \(\mathbb C\). With a complex-linear unital involution, \((i1)^*(i1)=-1\); a normalized functional takes this to \(-1\), contradicting square positivity. The earlier chosen bilinear adjoints likewise do not supply this Hermitian structure. No norm, continuity or operator representation is assumed.
Example 5. Square positivity need not imply real Hermiticity [fdip-0025]AGENTDRAFTED
- October 23, 2026
Example 5. Square positivity need not imply real Hermiticity [fdip-0025]AGENTDRAFTED
- October 23, 2026
In the real algebra \(A=\mathbb R[\varepsilon ]/(\varepsilon ^2)\), each element is uniquely \(x+y\varepsilon \). Define \((x+y\varepsilon )^*=x-y\varepsilon \). For any fixed real \(c\ne 0\), let \[\omega _c(x+y\varepsilon )=x+cy.\] Then \(\omega _c\) is normalized and nonnegative on every \(a^*a\), but is not a real algebraic state, because it is not Hermitian.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
The operation is real linear, fixes the unit and squares to the identity. Multiplication gives \((x+y\varepsilon )(u+v\varepsilon )=xu+(xv+yu)\varepsilon \); applying star negates the second coefficient, as does multiplying the starred factors. Since the algebra is commutative, this is also the required order-reversing product law. For \(a=x+y\varepsilon \), \(a^*a=(x-y\varepsilon )(x+y\varepsilon )=x^2\). Thus \(\omega _c(a^*a)=x^2\geq 0\), and \(\omega _c(1)=1\). But \(\omega _c(\varepsilon ^*)=-c\ne c=\omega _c(\varepsilon )\).
This direct calculation distinguishes square positivity from the extra real Hermiticity condition. Square positivity is defined in [waldmann2004states, Definition 3.9, p. 11]. It is separate from the characteristic-two group-algebra example: the present algebra and functional are over \(\mathbb R\).
Proposition 6. Finite states are probability weights [fdip-0026]AGENTDRAFTED
- October 23, 2026
Proposition 6. Finite states are probability weights [fdip-0026]AGENTDRAFTED
- October 23, 2026
Let \(\Omega \) be finite, \(K=\mathbb R\) or \(\mathbb C\), and give \(A_\Omega =\operatorname {Map}(\Omega ,K)\) the pointwise involution \(f^*(x)=\overline {f(x)}\). The weight functional \(\omega _p(f)=\sum _xp(x)f(x)\) is a real or complex algebraic state exactly when every \(p(x)\) is real and nonnegative and \(\sum _xp(x)=1\).
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Pointwise conjugation is additive, conjugates scalars, fixes the unit and is involutive. It reverses products because \(K\) is commutative. For necessity, \(\delta _x^*\delta _x=\delta _x\), so square positivity gives \(p(x)=\omega _p(\delta _x)\in \mathbb R_{\geq 0}\). Normalization gives the sum condition. Conversely, real weights imply \(\omega _p(f^*)=\sum _xp(x)\overline {f(x)}=\overline {\omega _p(f)}\). Furthermore \[\omega _p(f^*f)=\sum _xp(x)|f(x)|^2\geq 0,\] and \(\omega _p(1)=\sum _xp(x)=1\). For a real pointwise nonnegative function, each summand \(p(x)f(x)\) is also nonnegative, so its expectation is nonnegative.
There is no state on the empty configuration set over \(\mathbb R\) or \(\mathbb C\), because the empty sum is zero. On two points, the weights \(p(0)=p(1)=1/2\) give a state that is not multiplicative: \(\omega _p(\delta _0\delta _1)=0\), whereas \(\omega _p(\delta _0)\omega _p(\delta _1)=1/4\). A state is not required to be an algebra homomorphism.
The positive-functional convention is [waldmann2004states, Definition 3.9, p. 11]; the indicator calculation above identifies it with finite probability and expectation on this particular algebra. It does not identify positivity cones on arbitrary star algebras; the distinctions on [waldmann2004states, p. 12] remain separate.
Proposition 7. Pulling a functional back along a supplied algebra map [fdip-0027]AGENTDRAFTED
- October 23, 2026
Proposition 7. Pulling a functional back along a supplied algebra map [fdip-0027]AGENTDRAFTED
- October 23, 2026
Let \(R\) be a commutative unital ring, \(A,B\) unital associative \(R\)-algebras, and let \(\iota :B\to A\) be a supplied unital algebra homomorphism. Precomposition defines an \(R\)-linear map in the opposite direction on ordinary duals: \[\begin {aligned} \iota ^\flat :\operatorname {Hom}_R(A,R)&\longrightarrow \operatorname {Hom}_R(B,R),\\ \omega &\longmapsto \omega \circ \iota . \end {aligned}\] It sends normalized functionals to normalized functionals. For another unital associative \(R\)-algebra \(C\) and a unital \(R\)-algebra homomorphism \(\kappa :C\to B\), \[(\iota \circ \kappa )^\flat =\kappa ^\flat \circ \iota ^\flat , \qquad (\mathrm {id}_A)^\flat =\mathrm {id}.\] When \(\iota \) is inclusion this is literal restriction; for an injective map it becomes restriction after identifying \(B\) with its image. No injectivity is needed for precomposition itself. A partition of a set by itself does not supply an algebra map between arbitrary algebras.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
For \(b,c\in B\) and \(r,s\in R\), linearity of \(\iota \) and \(\omega \) gives \((\omega \iota )(rb+sc)=r(\omega \iota )(b)+s(\omega \iota )(c)\). Pointwise operations on the dual also give \((r\omega +s\nu )\iota =r(\omega \iota )+s(\nu \iota )\). Since \(\iota (1_B)=1_A\), normalization follows from \((\omega \iota )(1_B)=\omega (1_A)=1_R\). For every \(c\in C\), both sides of the composition identity take \(\omega \) to \(\omega (\iota (\kappa (c)))\); the identity law is immediate by evaluation.
Linearity and preservation of the unit suffice for the normalization calculation; multiplication preservation additionally respects observable products. Without unitality, the zero multiplicative linear map between nonzero real algebras pulls every normalized functional back to zero.
Over \(K=\mathbb R\) or \(\mathbb C\), suppose both algebras carry the star laws in the state definition, and suppose additionally \(\iota (b^*)=\iota (b)^*\). Then \(\iota ^\flat \) sends algebraic states to algebraic states. For composition in this setting, let \(C\) also be a unital associative \(K\)-algebra with these star laws, and let \(\kappa :C\to B\) be a unital \(K\)-algebra homomorphism preserving star.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
For a state \(\omega \), \((\omega \iota )(b^*)=\omega (\iota (b)^*)=\overline {\omega (\iota (b))}\). Multiplication and star compatibility give \[(\omega \iota )(b^*b)=\omega (\iota (b)^*\iota (b))\geq 0.\] Normalization holds. Identities preserve star, and \((\iota \kappa )(c^*)=\iota (\kappa (c)^*)=(\iota \kappa (c))^*\), so composition preserves the same hypotheses.
Star compatibility cannot be omitted. Give \(\mathbb C[z]\) the involution conjugating coefficients and fixing \(z\); give \(\mathbb C\) ordinary conjugation. Evaluation at \(z=i\) is a unital complex algebra map. The identity functional on \(\mathbb C\) is a state, but its pullback takes \(z^*z=z^2\) to \(-1\), so is not positive.
The dual-map construction is supported by Mathlib's
LinearMap.dualMap, LinearMap.dualMap_apply,
LinearMap.dualMap_id and LinearMap.dualMap_comp_dualMap;
these do not require finite dimension. The star-preserving map structures
StarAlgHom and StarAlgHom.comp concern supplied star
operations; the genuine star laws above remain explicit hypotheses.
For the algebra and positivity conventions see
[stacks2017stacks, Section 22.2], Tag 09JF and
[waldmann2004states, Definitions 3.7 and 3.9, p. 11].
The normalization and positivity assertions here are proved directly.
Proposition 8. Finite-map pullback and fiber weights [fdip-0028]AGENTDRAFTED
- October 23, 2026
Proposition 8. Finite-map pullback and fiber weights [fdip-0028]AGENTDRAFTED
- October 23, 2026
Let \(\rho :\Omega \to \Lambda \) be any map of finite sets and let \(R\) be a commutative unital ring. On the function algebras, \[\begin {aligned} \rho ^*:A_\Lambda &\longrightarrow A_\Omega ,& f&\longmapsto f\circ \rho \end {aligned}\] is a unital \(R\)-algebra map. Over \(\mathbb R\) or \(\mathbb C\) it preserves pointwise conjugation. For \(\tau :\Lambda \to \Gamma \), \((\tau \circ \rho )^*=\rho ^*\circ \tau ^*\), and the identity set map induces the identity algebra map.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
At \(x\in \Omega \), pullback of \(rf+sg\), \(fg\), and \(1\) has value \(rf(\rho (x))+sg(\rho (x))\), \(f(\rho (x))g(\rho (x))\), and \(1_R\), respectively. Pullback commutes with conjugation by the same evaluation. Both composite pullbacks evaluate \(f\) at \(\tau (\rho (x))\); the identity case evaluates \(f\) at \(x\). These pointwise arguments also apply to empty domains and the zero ring.
The image of \(\rho ^*\) consists exactly of functions constant on each fiber of \(\rho \). If \(\rho \) is surjective, \(\rho ^*\) is injective. Conversely, injectivity of \(\rho ^*\) forces surjectivity of \(\rho \) provided \(R\) is nonzero.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
A pullback takes equal values at \(x,x'\) whenever \(\rho (x)=\rho (x')\). Conversely, for fiber-constant \(g\), define \(f(y)\) to be the common value on the fiber when that fiber is nonempty, and \(0_R\) when it is empty. The value is independent of the chosen representative, and \(g=f\rho \). If \(\rho \) is surjective, equality of two pullbacks determines their value at every \(y\), proving injectivity. If \(y\) is missed, \(\delta _y\) pulls back to zero; for nonzero \(R\) this indicator is nonzero, so pullback is not injective. Over the zero ring, all these algebras are singletons and every pullback is injective, including pullback along a nonsurjective set map.
For the weight functional determined by \(p\), its pullback as a functional along \(\rho ^*\) has weights \[q(y)=\sum _{\rho (x)=y}p(x).\] Thus normalized weights stay normalized; real nonnegative weights stay nonnegative. Empty fibers have weight zero.
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Regroup the finite sum: \[\begin {aligned} (\omega _p\circ \rho ^*)(f) &=\sum _{x\in \Omega }p(x)f(\rho (x))\\ &=\sum _{y\in \Lambda }\left (\sum _{\rho (x)=y}p(x)\right )f(y). \end {aligned}\] The fibers partition \(\Omega \), so \(\sum _yq(y)=\sum _xp(x)\). Nonnegative summands give nonnegative fiber sums. For successive maps, \[\sum _{\tau (y)=z}\sum _{\rho (x)=y}p(x) =\sum _{\tau (\rho (x))=z}p(x),\] which proves compatibility of the fiber formula with composition.
For real nonnegative weights of total one, this is
pushforward of finite probabilities, or a marginal law
when \(\rho \) forgets coordinates. It uses no division by
fiber mass, even when that mass is zero; it is not a conditional
expectation. The pointwise algebra construction uses
[stacks2017stacks, Section 22.2], Tag 09JF.
Mathlib's AlgHom.pi constructs the family of evaluation maps
\(f\mapsto f(\rho (x))\). Composition here changes the function's domain,
not its coefficient ring.
Over arbitrary rings, not every unital algebra map between function algebras is induced by a set map. For \(R=\mathbb Z/6\mathbb Z\), define \(h:R^2\to R\) by \(h(a,b)=3a+4b\). It is \(R\)-linear and unital since \(3+4=1\). The identities \(3^2=3\), \(4^2=4\), and \(3\cdot 4=0\) show \(h(a,b)h(c,d)=3ac+4bd=h(ac,bd)\), so it is multiplicative. But \(h(1,0)=3\), whereas either coordinate evaluation gives \(0\) or \(1\). Thus this map is not the pullback of a map from a singleton to two points.
Example 9. A nonuniform law on sixteen cycle configurations [fdip-0029]AGENTDRAFTED
- October 23, 2026
Example 9. A nonuniform law on sixteen cycle configurations [fdip-0029]AGENTDRAFTED
- October 23, 2026
Use the 4 vertices \(V=\{0,1,2,3\}\) of the alternating cycle, the alphabet \(S=\{0,1\}\), and retained vertices \(J=\{0,2\}\). There are 16 configurations \(\Omega =S^V\) and 4 retained configurations \(\Lambda =S^J\). The map \(\rho (\sigma )=\sigma |_J\) is surjective: assign zero at vertices \(1,3\) to extend any retained configuration. Each fiber has 4 elements. The pullback identifies retained observables with those depending only on the values at vertices \(0,2\).
Choose the following real weights, independently of the edge energies: \[p(\sigma )=\begin {cases} 1/12,&\sigma _0=\sigma _2,\\ 1/24,&\sigma _0\ne \sigma _2. \end {cases}\] There are 8 configurations of each kind, so \(\sum _\sigma p(\sigma )=8/12+8/24=1\). By the finite-state criterion, this defines a real algebraic state. Summing the 4 weights in each fiber gives \[q(0,0)=q(1,1)=1/3,\qquad q(0,1)=q(1,0)=1/6.\] For \(F(\eta )=\eta _0\eta _2\), only \(\eta =(1,1)\) contributes, and hence \[\omega _q(F)=1/3=4\cdot (1/12)=\omega _p(F\circ \rho ).\] This is an explicit instance of the finite fiber-sum identity.
The law here is a chosen finite probability distribution. It is not obtained from the cycle's edge weights or its precision matrix, and the carrier \(S^V\) is distinct from the real configuration space \(\mathbb R^V\) used by the Gaussian law. The algebra convention remains [stacks2017stacks, Section 22.2], Tag 09JF; the positivity convention is [waldmann2004states, Definition 3.9, p. 11]. If the vertex set is empty, \(S^\varnothing \) has one outcome, even for empty \(S\). An empty alphabet with nonempty vertex set instead gives no outcomes and no real state. Thus zero vertices and an empty configuration set are different cases.
Proposition 10. Pullback of polynomial functions [fdip-002A]AGENTDRAFTED
- October 23, 2026
Proposition 10. Pullback of polynomial functions [fdip-002A]AGENTDRAFTED
- October 23, 2026
Let \(V\) be finite, \(J\subseteq V\), \(X=\mathbb R^V\) and \(Y=\mathbb R^J\). Let \(\pi :X\to Y\) restrict a configuration to \(J\). Write \(\mathcal P(X)\) and \(\mathcal P(Y)\) for the algebras of real polynomial functions generated by the coordinate evaluation functions, with pointwise operations and the identity involution. Then \[\begin {aligned} \pi ^*:\mathcal P(Y)&\longrightarrow \mathcal P(X),& P&\longmapsto P\circ \pi \end {aligned}\] is an injective unital real algebra map preserving these involutions. Every supplied real algebraic state on \(\mathcal P(X)\) therefore pulls back to one on \(\mathcal P(Y)\).
Proof.
- October 23, 2026
Proof.
- October 23, 2026
Each coordinate function \(y\mapsto y_j\), \(j\in J\), pulls back to \(x\mapsto x_j\). Composition preserves sums, products, real scalar multiples and constants by pointwise evaluation. Consequently a polynomial function pulls back to a polynomial function and \(\pi ^*\) is a unital real algebra map. Both involutions are the identity, so it preserves star. Define \(s:Y\to X\) by filling coordinates outside \(J\) with zero. Then \(\pi \circ s=\mathrm {id}_Y\). If \(P\circ \pi =Q\circ \pi \), composition with \(s\) gives \(P=Q\), proving injectivity. The state pullback proposition now applies to a supplied state. These arguments also cover \(J=\varnothing \) and \(V=\varnothing \); their real coordinate spaces are singletons, not empty sets.
Here polynomial functions are actual functions, rather than formal polynomial expressions. The proof uses coordinate composition and the zero-fill section, not a finiteness assertion about the real set \(X\). The algebra and positivity conventions are [stacks2017stacks, Section 22.2], Tag 09JF and [waldmann2004states, Definition 3.9, p. 11]. The finite-map construction gives the same contravariant direction, but its finite indicator expansion is not used here.
For the Gaussian expectation, measure and polynomial integrability first establishes that the Gaussian polynomial state on \(\mathcal P(X)\) exists. Once supplied, it restricts by the algebraic result above. Identifying its retained law requires the separate Gaussian marginal calculation. This proposition neither extends that analytic calculation to new degenerate cases nor asserts that all integrable functions form an algebra. Polynomial functions are also distinct from the algebra of field endomorphisms.