module Cat.Abelian.Instances.Ab {ℓ} where
The category of abelian groups🔗
The prototypal — representative, even — example of an ,
and an abelian
category at that, is the category of abelian groups,
For abstractly-nonsensical reasons, we could say
is
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 (∫hom (λ _ → lift tt) (record { pres-⋆ = λ x y i → lift tt })) λ x → trivial! Ab-is-additive .has-prods A B .apex = A ⊕ B Ab-is-additive .has-prods A B .π₁ = _ Ab-is-additive .has-prods A B .π₂ = _ Ab-is-additive .has-prods A B .has-is-product = Direct-sum-is-product