Documentation

Mathlib.Algebra.Category.Grp.Injective

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 #

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.

instance AddCommGrp.injective_of_divisible (A : Type u) [AddCommGroup A] [DivisibleBy A ] :
CategoryTheory.Injective { α := A, str := inferInstance }
Equations
  • =