The category of abelian groups is abelian
In the category of abelian groups, every monomorphism is normal.
In the category of abelian groups, every epimorphism is normal.
@[instance]
The category of abelian groups is abelian.
Equations
- AddCommGroup.category_theory.abelian = {to_preadditive := {hom_group := λ (P Q : AddCommGroup), category_theory.preadditive.hom_group P Q, add_comp' := AddCommGroup.category_theory.abelian._proof_1, comp_add' := AddCommGroup.category_theory.abelian._proof_2}, has_finite_products := id (λ (J : Type) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape_of_has_limits), has_kernels := category_theory.limits.has_kernels_of_has_equalizers AddCommGroup category_theory.limits.has_limits_of_shape_of_has_limits, has_cokernels := category_theory.limits.has_cokernels_of_has_coequalizers AddCommGroup category_theory.limits.has_colimits_of_shape_of_has_colimits, normal_mono := λ (X Y : AddCommGroup), AddCommGroup.normal_mono, normal_epi := λ (X Y : AddCommGroup), AddCommGroup.normal_epi}