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 ring1. 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.

1. We tacitly assume the reader has a favourite ring.↩︎