# Injective objects in the category of abelian groups #

In this file we prove that divisible groups are injective object in category of (additive) abelian groups and that the category of abelian groups has enough injective objects.

## Main results #

`AddCommGrp.injective_of_divisible`

: a divisible group is also an injective object.`AddCommGrp.enoughInjectives`

: the category of abelian groups (written additively) has enough injectives.`CommGrp.enoughInjectives`

: the category of abelian group (written multiplicatively) has enough injectives.

## Implementation notes #

The details of the proof that the category of abelian groups has enough injectives is hidden
inside the namespace `AddCommGroup.enough_injectives_aux_proofs`

. These are not marked `private`

,
but are not supposed to be used directly.

theorem
AddCommGrp.injective_as_module_iff
(A : Type u)
[AddCommGroup A]
:

CategoryTheory.Injective (ModuleCat.mk A) ↔ CategoryTheory.Injective { α := A, str := inferInstance }

instance
AddCommGrp.injective_of_divisible
(A : Type u)
[AddCommGroup A]
[DivisibleBy A ℤ]
:

CategoryTheory.Injective { α := A, str := inferInstance }

## Equations

- ⋯ = ⋯