Documentation

Mathlib.Algebra.Category.Grp.EnoughInjectives

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.