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 Module.Baer.of_divisible (A : Type u) [AddCommGroup A] [DivisibleBy A ℤ] : Module.Baer ℤ A

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

• ⋯ = ⋯

instance AddCommGrp.injective_ratCircle : CategoryTheory.Injective (AddCommGrp.of (ULift.{u, 0} (AddCircle 1)))

Equations

• AddCommGrp.injective_ratCircle = ⋯