Proposition. Transport of polynomial observables and functionals [fdip-003F]
✍️source

  • October 29, 2026

Let \(k\) be a commutative unital ring. For a \(k\)-module \(M\), write \(\mathcal P_k(M)\) for the unital \(k\)-subalgebra of functions \(M\to k\) generated by ordinary linear functionals. This extends the intrinsic real polynomial functions using the same pointwise operations. These are actual functions: over finite fields, distinct formal polynomials can have identical evaluations.

For a linear isomorphism \(P:M\to M'\), pullback gives a unital algebra isomorphism \[P^*:\mathcal P_k(M')\longrightarrow \mathcal P_k(M),\qquad P^*F'=F'\circ P.\] An already supplied normalized functional \(\omega \) on \(\mathcal P_k(M)\) transports to \(\omega '=\omega \circ P^*\). For the moving split square, the retained functionals \(\omega _X=\omega \circ \pi ^*\) and \(\omega '_{X'}=\omega '\circ (\pi ')^*\) satisfy \[\omega '_{X'}=\omega _X\circ P_X^*.\] Here \(\pi :M\to X\), \(\pi ':M'\to X'\) are the specified projections, and \(\pi 'P=P_X\pi \).

Proof. 

  • October 29, 2026

Precomposition preserves sums, scalar multiples, products and the constant function \(1\), by evaluation. A linear functional on \(M'\) composed with \(P\) is linear on \(M\), so pullback preserves the generated polynomial algebras. Its inverse is \((P^{-1})^*\). For composable maps, \((P'P)^*F''=F''\circ P'\circ P=P^*((P')^*F'')\); identity pullback is identity. This proves contravariance as well.

Linearity of \(\omega '\) and \(\omega '(1)=\omega (1)=1\) follow directly, or by algebra-map pullback. The section \(\iota _X\) of \(\pi \) makes \(\pi ^*\) injective: \(f\circ \pi =g\circ \pi \) implies \(f=g\) after composition with \(\iota _X\). Thus \(\omega _X\) is restriction to the image of \(\pi ^*\), identified with \(\mathcal P_k(X)\). Finally, for each \(f'\in \mathcal P_k(X')\) and \(x\in M\), \[\begin {aligned} P^*(\pi ')^*f'(x) &=f'(\pi 'Px)\\ &=f'(P_X\pi x)=(\pi ^*P_X^*f')(x). \end {aligned}\] Applying \(\omega \) gives the asserted retained-functional equality.

Over \(\mathbb R\) with the identity involution, or over \(\mathbb C\) with pointwise conjugation, suppose the chosen observable algebras are closed under that involution. Pullback then commutes with star. If \(\omega \) is an algebraic state, \[\begin {aligned} \omega '(F'^*F') &=\omega \bigl ((P^*F')^*(P^*F')\bigr )\geq 0, \end {aligned}\] and the star compatibility of the functional is preserved too. Holomorphic polynomial functions on a complex vector space are not automatically closed under conjugation; closure is an extra hypothesis. One can instead generate an algebra by both linear functionals and their conjugates; precomposition preserves those generators as well. No positivity over an arbitrary ring or existence of a measure is asserted. For the real Gaussian, absolute moments first give its polynomial state; the transported law then identifies this algebraic transport with expectation. Integrable functions as a whole are not an algebra, and restriction here is neither conditional expectation nor partial trace.

The algebra and state conventions are [stacks2017stacks, Section 22.2], Tag 09JF and [waldmann2004states, Definitions 3.7 and 3.9, p. 11]. The composition and split-square calculations are direct extensions of Proposition [fdip-002A] and Proposition [fdip-0027]; their linear-dual and star-algebra interfaces do not supply a Gaussian measure.