# The precategory of abelian groups

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-05-06.

module group-theory.precategory-of-abelian-groups where

Imports
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.homomorphisms-abelian-groups


## Idea

The precategory of abelian groups consists of abelian groups and group homomorphisms.

## Definition

### The large precategory of abelian groups

Ab-Large-Precategory : Large-Precategory lsuc (_⊔_)
Large-Precategory.obj-Large-Precategory
Ab-Large-Precategory =
Ab
Large-Precategory.hom-set-Large-Precategory
Ab-Large-Precategory =
hom-set-Ab
Large-Precategory.comp-hom-Large-Precategory
Ab-Large-Precategory {X = A} {B} {C} =
comp-hom-Ab A B C
Large-Precategory.id-hom-Large-Precategory
Ab-Large-Precategory {X = A} =
id-hom-Ab A
Large-Precategory.associative-comp-hom-Large-Precategory
Ab-Large-Precategory {X = A} {B} {C} {D} =
associative-comp-hom-Ab A B C D
Large-Precategory.left-unit-law-comp-hom-Large-Precategory
Ab-Large-Precategory {X = A} {B} =
left-unit-law-comp-hom-Ab A B
Large-Precategory.right-unit-law-comp-hom-Large-Precategory
Ab-Large-Precategory {X = A} {B} =
right-unit-law-comp-hom-Ab A B


### The small categories of abelian groups

Ab-Precategory : (l : Level) → Precategory (lsuc l) l
Ab-Precategory = precategory-Large-Precategory Ab-Large-Precategory