The precategory of abelian groups

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor and louismntnu

Created on 2023-05-06.
Last modified on 2023-06-25.

module group-theory.precategory-of-abelian-groups where
Imports 
open import category-theory.large-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-Precategory : Large-Precategory lsuc (_⊔_)
Large-Precategory.obj-Large-Precategory ab-Precategory = Ab
Large-Precategory.hom-Large-Precategory ab-Precategory = hom-Ab
Large-Precategory.comp-hom-Large-Precategory ab-Precategory
  {X = A} {B} {C} =
  comp-hom-Ab A B C
Large-Precategory.id-hom-Large-Precategory ab-Precategory
  {X = A} =
  id-hom-Ab A
Large-Precategory.associative-comp-hom-Large-Precategory ab-Precategory
  {X = A} {B} {C} {D} =
  associative-comp-hom-Ab A B C D
Large-Precategory.left-unit-law-comp-hom-Large-Precategory ab-Precategory
  {X = A} {B} =
  left-unit-law-comp-hom-Ab A B
Large-Precategory.right-unit-law-comp-hom-Large-Precategory ab-Precategory
  {X = A} {B} =
  right-unit-law-comp-hom-Ab A B

Recent changes