Injective objects in the category of abelian groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that divisible groups are injective object in category of (additive) abelian groups.
theorem
AddCommGroup.injective_of_injective_as_module
(A : Type u)
[add_comm_group A]
[category_theory.injective (Module.mk A)] :
category_theory.injective {α := A, str := _inst_1}
theorem
AddCommGroup.injective_as_module_of_injective_as_Ab
(A : Type u)
[add_comm_group A]
[category_theory.injective {α := A, str := _inst_1}] :
@[protected, instance]
def
AddCommGroup.injective_of_divisible
(A : Type u)
[add_comm_group A]
[divisible_by A ℤ] :
category_theory.injective {α := A, str := _inst_1}