# The category of abelian groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-17.

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

Imports
open import category-theory.categories
open import category-theory.full-large-subcategories
open import category-theory.functors-large-categories
open import category-theory.large-categories
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.category-of-groups


## Idea

The category of abelian groups is the full large subcategory of the category of groups consisting of groups of which the group operation is commutative.

## Definitions

### The large category of abelian groups

Ab-Large-Category : Large-Category lsuc (_⊔_)
Ab-Large-Category =
large-category-Full-Large-Subcategory
( Group-Large-Category)
( is-abelian-prop-Group)


### The large precategory of abelian groups

Ab-Large-Precategory : Large-Precategory lsuc (_⊔_)
Ab-Large-Precategory =
large-precategory-Large-Category Ab-Large-Category


### The category of abelian groups of a given universe level

Ab-Category : (l : Level) → Category (lsuc l) l
Ab-Category = category-Large-Category Ab-Large-Category


### The precategory of abelian groups of a given universe level

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


### The forgetful functor from abelian groups to groups

forgetful-functor-Ab :
functor-Large-Category (λ l → l) Ab-Large-Category Group-Large-Category
forgetful-functor-Ab =
forgetful-functor-Full-Large-Subcategory
( Group-Large-Category)
( is-abelian-prop-Group)