module Cat.Abelian.Endo {o β„“} {C : Precategory o β„“} (A : Ab-category C) where

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.


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