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.Grp.Injective is to prevent import loop.
This file's dependency imports Mathlib.Algebra.Grp.Injective.