Category of abelian groups has enough injectives #
Given an abelian group A, then i : A ⟶ ∏_{A⋆} ℚ ⧸ ℤ defined by i : a ↦ c ↦ c a is an
injective presentation for A, hence category of abelian groups has enough injectives.
Implementation notes #
This file is split from Mathlib.Algebra.Category.Grp.Injective to prevent import loops.