module Cat.Abelian.Instances.Ab {β„“} where

The category of abelian groupsπŸ”—

The prototypal β€” representative, even β€” example of an Ab\mathbf{Ab}-enriched, and an abelian category at that, is the category of abelian groups, Ab\mathbf{Ab}. For abstractly-nonsensical reasons, we could say Ab\mathbf{Ab} is Ab\mathbf{Ab}-enriched by virtue of being monoidal closed, but we have a concrete construction at hand: Ab-ab-category

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-category
Ab-is-additive .has-terminal .top = from-commutative-group (Zero-group {β„“}) (Ξ» x y β†’ refl)
Ab-is-additive .has-terminal .has⊀ x =
  contr (total-hom (Ξ» _ β†’ lift tt) (record { pres-⋆ = Ξ» x y i β†’ lift tt }))
    Ξ» x β†’ Homomorphism-path Ξ» _ β†’ 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