Definition. Normalized linear functionals [fdip-0021]
AGENTDRAFTED
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.
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.