open import Algebra.Group.Cat.FinitelyComplete open import Algebra.Group.Cat.Base open import Algebra.Group.Subgroup open import Algebra.Group.Ab.Free open import Algebra.Group.Ab.Sum open import Algebra.Group.Ab open import Algebra.Group open import Cat.Functor.Adjoint.Continuous open import Cat.Diagram.Equaliser.Kernel open import Cat.Functor.FullSubcategory open import Cat.Diagram.Coequaliser open import Cat.Diagram.Equaliser open import Cat.Diagram.Terminal open import Cat.Diagram.Product open import Cat.Functor.Adjoint open import Cat.Abelian.Base open import Cat.Prelude module Cat.Abelian.Instances.Ab {β} where
The category of abelian groupsπ
The prototypal β representative, even β example of an -enriched, and an abelian category at that, is the category of abelian groups, . For abstractly-nonsensical reasons, we could say is -enriched by virtue of being monoidal closed, but we have a concrete construction at hand to apply. Letβs see it:
Ab-ab : Ab-category (Ab β) Ab-ab .Group-on-hom A B = Hom-group A B .Restrict-ob.object .snd Ab-ab .Hom-grp-ab A B = Hom-group A B .Restrict-ob.witness Ab-ab .β-linear-l f g h = Forget-is-faithful refl Ab-ab .β-linear-r f g h = Forget-is-faithful $ funext Ξ» x β sym $ f .preserves .Group-hom.pres-β _ _
Let us show it is additive. The terminal group is given by the terminal set, equipped with its unique group structure, and we have already computed products β they are given by direct sums.
Ab-is-additive : is-additive (Ab β) Ab-is-additive .has-ab = Ab-ab Ab-is-additive .has-terminal .top = restrict (to-group p) Ξ» _ _ β refl where p : make-group (Lift _ β€) p .group-is-set a b p q i j = lift tt p .unit = lift tt p .mul _ _ = lift tt p .inv _ = lift tt p .assoc x y z i = lift tt p .invl x i = lift tt p .invr x i = lift tt p .idl x i = lift tt Ab-is-additive .has-terminal .hasβ€ x = contr (total-hom (Ξ» _ β lift tt) record { pres-β = Ξ» _ _ β refl }) Ξ» h β Forget-is-faithful refl Ab-is-additive .has-prods A B .Product.apex = A β B Ab-is-additive .has-prods A B .Product.Οβ = _ Ab-is-additive .has-prods A B .Product.Οβ = _ Ab-is-additive .has-prods A B .Product.has-is-product = Direct-sum-is-product