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

private module A = Ab-category A


# Endomorphism ringsπ

Fix an It can be the category of abelian groups itself, for example, or for your favourite ring1. Because composition in distributes over addition, the collection of endomorphisms of any particular object is not only a monoid, but a ring: the endomorphism ring of

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 it is an open problem to characterise the abelian groups with commutative endomorphism rings.