# Documentation

Mathlib.Algebra.Category.GroupCat.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 #

• AddCommGroupCat.injective_of_divisible : a divisible group is also an injective object.
• AddCommGroupCat.enoughInjectives : the category of abelian groups 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.

The next term of A's injective resolution is ∏_{A →+ ℚ/ℤ}, ℚ/ℤ.

Instances For

The map into the next term of A's injective resolution is coordinate-wise evaluation.

Instances For

ℤ ⧸ ⟨ord(a)⟩ ≃ aℤ

Instances For
↑() { val := a, property := (_ : a ) } =
@[inline, reducible]

Given n : ℕ, the map m ↦ m / n.

Instances For
@[simp]
∀ (a : { x // x }), AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle a = ↑(Submodule.liftQSpanSingleton (↑()) (AddCommGroupCat.enough_injectives_aux_proofs.divBy (if = 0 then 2 else )) (_ : ↑(AddCommGroupCat.enough_injectives_aux_proofs.divBy (if = 0 then 2 else )) ↑() = 0)) (↑(Submodule.quotEquivOfEq (LinearMap.ker ()) (Ideal.span {↑()}) (_ : LinearMap.ker () = Ideal.span {↑()})) (↑() (↑(LinearEquiv.ofEq () (LinearMap.range ()) (_ : = LinearMap.range ())) a)))

The map sending n • a to n / 2 when a has infinite order, and to n / addOrderOf a otherwise.

Instances For
theorem AddCommGroupCat.enough_injectives_aux_proofs.eq_zero_of_toRatCircle_apply_self {A_ : AddCommGroupCat} {a : A_} (h : AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle { val := a, property := (_ : a ) } = 0) :
a = 0

An injective presentation of A: A → ∏_{A →+ ℚ/ℤ}, ℚ/ℤ.

Instances For