Definition. Chosen perfect symmetric pairings [fdip-001O]
AGENTDRAFTED
The perfect counting duality represents every
linear functional by a unique field. To make the same construction on
another carrier, let \(R\) be a commutative unital ring
and \(M\) a unital \(R\)-module. Write
\(M^\vee =\operatorname {Hom}_R(M,R)\) for its
dual module. Every linear map here has coefficient
map \(\operatorname {id}_R\), as in Remark [ca-001G].
A chosen perfect symmetric pairing on \(M\) is a
bilinear form \(b_M:M\times M\to R\) such that
\(b_M(x,y)=b_M(y,x)\) and the linear map
\[\Phi _M:M\longrightarrow M^\vee ,\qquad
\Phi _M(y)(x)=b_M(x,y)\]
is an isomorphism. Thus each functional \(\ell \)
has exactly one representative \(\Phi _M^{-1}\ell \), characterized by
\(b_M(x,\Phi _M^{-1}\ell )=\ell (x)\) for every \(x\). Bilinearity makes
\(\Phi _M\) linear. Symmetry identifies the other currying map
\(y\mapsto (x\mapsto b_M(y,x))\) with \(\Phi _M\), so both are
isomorphisms. This agrees with the two-sided perfect-pairing convention
in Mathlib's LinearMap.IsPerfPair. The ordinary Hom convention
is [stacks2017stacks, Section 10.10], Tag 0581.
Injectivity alone says that \(b_M(x,y)=0\) for every \(x\) forces
\(y=0\); symmetry gives the analogous assertion in the other slot.
It does not give every functional a representative; see
a zero-radical pairing that is not perfect.
No finiteness, basis or projectivity hypothesis is imposed on \(M\);
the specified duality is the assumption. The counting form on every
finite function module satisfies it by the explicit inverse in
Lemma [fdip-001F]. The zero module has its unique perfect pairing.
If \(R\) is the zero ring, every unital module is zero since
\(x=1x=0x=0\), so this case is included. Perfection does not assert
positivity or determine a bilinear form from its diagonal values.