English
For a commutative ring R with an involution (star operation), the endomorphism ring consisting of star-endomorphisms carries a canonical involutive pair of ring homomorphisms. Concretely, taking the star of an endomorphism gives a ring endomorphism, and applying star twice yields the original endomorphism.
Русский
Для коммутативного кольца R с инволюцией (операцией *) множество концевых отображений R, замыкающихся на звездку, образует каноническую пару противообратимых кольцевых однородных отображений. Конкретно: операция звезды на отображении даёт новое кольцевое отображение, и применение звезды два раза возвращает исходное отображение.
LaTeX
$$$\exists \alpha, \beta : \mathrm{End}(\star\text{RingEnd}(R))\; (\alpha, \beta) \text{ — кольцевые гомоморфизмы}, \alpha = \beta^{-1}, \alpha(x) = \star x \text{ для всех } x.$$$
Lean4
/-- Instance needed to define star-linear maps over a commutative star ring
(ex: conjugate-linear maps when R = ℂ). -/
instance [CommSemiring R] [StarRing R] : RingHomInvPair (starRingEnd R) (starRingEnd R) :=
⟨RingHom.ext star_star, RingHom.ext star_star⟩
