Definition. Chosen perfect symmetric pairings [fdip-001O]

✍️sourceAGENTDRAFTED

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.