module Cat.Abelian.Endo {o β} {C : Precategory o β} (A : Ab-category C) where
Endomorphism ringsπ
Fix an -category : It can be the category of abelian groups itself, for example, or -Mod 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.
We tacitly assume the reader has a favourite ring.β©οΈ