Proposition. Adjoints from chosen dualities [fdip-001P]
AGENTDRAFTED
Let \(R\) be a commutative unital ring and let \(M,N,P\) be unital
\(R\)-modules with chosen perfect symmetric pairings
\(b_M,b_N,b_P\) and duality maps \(\Phi _M,\Phi _N,\Phi _P\).
For an ordinary \(R\)-linear map \(A:M\to N\),
precomposition defines
\[A^\vee :N^\vee \longrightarrow M^\vee ,\qquad A^\vee \ell =\ell \circ A.\]
Its adjoint for chosen perfect pairings is
\[A^\dagger =\Phi _M^{-1}A^\vee \Phi _N:N\longrightarrow M.\]
Products denote composition, with the right factor first, as in
composition and field multiplication.
This is the unique linear map satisfying
\[b_M(x,A^\dagger y)=b_N(Ax,y)\qquad (x\in M,\ y\in N).\]
For \(A,A':M\to N\), \(B:N\to P\) and \(r\in R\),
\[\begin {aligned}
(A+A')^\dagger &=A^\dagger +(A')^\dagger ,&
(rA)^\dagger &=rA^\dagger ,\\
0^\dagger &=0,&I_M^\dagger &=I_M,\\
(BA)^\dagger &=A^\dagger B^\dagger ,&
(A^\dagger )^\dagger &=A.
\end {aligned}\]
If \(A\) is an isomorphism, then \(A^\dagger \) is an isomorphism and
\[(A^{-1})^\dagger =(A^\dagger )^{-1}.\]
An endomorphism \(L:M\to M\) is self-adjoint for this
pairing when \(L^\dagger =L\). In particular, the inverse of an
invertible self-adjoint endomorphism is self-adjoint.
In particular, for \(d:M\to N\) and a self-adjoint
\(W:N\to N\), the composite \(L=d^\dagger Wd:M\to M\) satisfies
\[L^\dagger =d^\dagger W^\dagger d=L,\qquad
b_M(f,Lg)=b_N(df,Wdg).\]
The first equality uses product reversal and double adjunction; the
second is the characterizing identity for \(d\). Taking \(g=f\) gives
its energy identity, without any order assumption on \(R\).
For a finite function module with its counting form,
\(\Phi ^{-1}=\Psi \) from Lemma [fdip-001F]; the formula is exactly
\(\Psi A^\vee \Phi \) from Proposition [fdip-001H]. Hence it gives the same
ordinary \(R\)-linear involution on endomorphisms.
The proof above extends that direct construction to different carriers.
The Hom convention is [stacks2017stacks, Section 10.10], Tag 0581.
TauCeti's Module.dualEndAlgEquiv expresses
reversed dual composition for reflexive modules. It concerns dual
endomorphisms, before the chosen symmetric identifications used here.
Mathlib's LinearMap.BilinForm.toDual constructs a duality
from a nondegenerate form in the finite-dimensional field case.
Here the dualities are explicitly assumed over \(R\); the argument above
proves the resulting adjoint laws. A nontrivial coefficient involution
and Hermitian forms require different scalar conventions.