Proposition. Pulling a functional back along a supplied algebra map [fdip-0027]
AGENTDRAFTED
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.
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.
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.