Definition. Ordinary linear involutions [fdip-001G]

✍️sourceAGENTDRAFTED

Let \(R\) be a commutative unital ring and \(A\) an associative unital \(R\)-algebra. An ordinary \(R\)-linear involution on \(A\) is an \(R\)-linear map \(a\mapsto a^\dagger \), with \(\sigma =\operatorname {id}_R\), satisfying \[1^\dagger =1,\qquad (ab)^\dagger =b^\dagger a^\dagger ,\qquad (a^\dagger )^\dagger =a.\] Thus it reverses products, preserves sums and satisfies \((ra)^\dagger =ra^\dagger \). The involution on the coefficient ring is explicitly the identity.

These are ordinary product-reversal laws: no sign depending on degree occurs. Over \(\mathbb C\), this convention is bilinear and does not introduce complex conjugation. A Hermitian adjoint needs different coefficient data. Neither a grading nor freeness selects an involution; the counting adjoint below is constructed from a specified pairing.

Mathlib separates the involutive law InvolutiveStar, product reversal StarMul, additive compatibility StarRing and scalar compatibility StarModule. Its starRingOfComm permits the identity involution on a commutative ring. These interfaces support the stated convention; the represented example requires its own proof. For the library attribution, see [mathlib2020lean].