This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The category of abelian groups

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

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)