Injective objects in the category of abelian groups

In this file we prove that divisible groups are injective objects in category of (additive) abelian groups. The proof that the category of abelian groups has enough injective objects can be found in Mathlib/Algebra/Category/Grp/EnoughInjectives.lean.

Main results

• AddCommGrp.injective_of_divisible : a divisible group is also an injective object.

theorem Module.Baer.of_divisible (A : Type u) [AddCommGroup A] [DivisibleBy A ℤ] : Baer ℤ A

theorem AddCommGrp.injective_as_module_iff (A : Type u) [AddCommGroup A] : CategoryTheory.Injective (ModuleCat.of ℤ A) ↔ CategoryTheory.Injective (of A)

instance AddCommGrp.injective_of_divisible (A : Type u) [AddCommGroup A] [DivisibleBy A ℤ] : CategoryTheory.Injective (of A)