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 Ab{{\mathbf{Ab}}}-category A\mathcal{A}: It can be the category of abelian groups Ab{{\mathbf{Ab}}} itself, for example, or RR-Mod for your favourite ring1. Because composition in A\mathcal{A} distributes over addition, the collection of endomorphisms of any particular object x:Ax : \mathcal{A} is not only a monoid, but a ring: the endomorphism ring of xx.

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 =
  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 A=Ab\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.β†©οΈŽ