Definition. Normalized linear functionals [fdip-0021]

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.