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 = to-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 = A.Hom.associative mr .+-comm = A.Hom.commutes mr .*-idl = A.idl _ mr .*-idr = A.idr _ mr .*-assoc = 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.β©οΈ