open import Algebra.Ring open import Cat.Abelian.Base open import Cat.Prelude module Cat.Abelian.Endo {o β} {C : Precategory o β} (A : Ab-category C) where

# Endomorphism ringsπ

Fix an ${{\mathbf{Ab}}}$-category
$\mathcal{A}$:
It can be the category of abelian groups
${{\mathbf{Ab}}}$
itself, for example, or
$R$-Mod
for your favourite ring^{1}. Because composition in
$\mathcal{A}$
distributes over addition, the collection of endomorphisms of any
particular object
$x : \mathcal{A}$
is not only a monoid, but a *ring*: the **endomorphism
ring** of
$x$.

Endo : A.Ob β Ring β Endo x = from-make-ring mr where open make-ring mr : make-ring (A.Hom x x) mr .ring-is-set = A.Hom-set x x mr .0R = A.0m mr .1R = A.id mr .make-ring._+_ = A._+_ mr .make-ring.-_ = A.Hom.inverse mr .make-ring._*_ = A._β_ mr .+-idl = A.Hom.idl mr .+-invr = A.Hom.inverser mr .+-assoc = sym A.Hom.associative mr .+-comm = A.Hom.commutative mr .*-idl = A.idl _ mr .*-idr = A.idr _ mr .*-assoc = sym (A.assoc _ _ _) mr .*-distribl = sym (A.β-linear-r _ _ _) mr .*-distribr = sym (A.β-linear-l _ _ _)

This is a fantastic source of non-commutative rings, and indeed the justification for allowing them at all. Even for the relatively simple case of $\mathcal{A} = {{\mathbf{Ab}}}$, it is an open problem to characterise the abelian groups with commutative endomorphism rings.

We tacitly assume the reader has a favourite ring.β©οΈ