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.

theorem AddCommGroupCat.injective_as_module_iff (A : Type u) [AddCommGroup A] : CategoryTheory.Injective (ModuleCat.mk A) ↔ CategoryTheory.Injective (CategoryTheory.Bundled.mk A)

instance AddCommGroupCat.injective_of_divisible (A : Type u) [AddCommGroup A] [DivisibleBy A ℤ] : CategoryTheory.Injective (CategoryTheory.Bundled.mk A)

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

def AddCommGroupCat.enough_injectives_aux_proofs.next (A_ : AddCommGroupCat) : AddCommGroupCat

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

instance AddCommGroupCat.enough_injectives_aux_proofs.instInjectiveAddCommGroupCatInstAddCommGroupCatLargeCategoryNext (A_ : AddCommGroupCat) : CategoryTheory.Injective (AddCommGroupCat.enough_injectives_aux_proofs.next A_)

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_apply (A_ : AddCommGroupCat) (a : ↑A_) (i : A_ ⟶ AddCommGroupCat.of (ULift.{u, 0} (AddCircle 1))) : ↑(AddCommGroupCat.enough_injectives_aux_proofs.toNext A_) a i = ↑i a

def AddCommGroupCat.enough_injectives_aux_proofs.toNext (A_ : AddCommGroupCat) : A_ ⟶ AddCommGroupCat.enough_injectives_aux_proofs.next A_

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

theorem LinearMap.toSpanSingleton_ker {A_ : AddCommGroupCat} (a : ↑A_) : LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a) = Ideal.span {↑(addOrderOf a)}

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf_apply {A_ : AddCommGroupCat} (a : ↑A_) : ∀ (a : { x // x ∈ Submodule.span ℤ {a} }), ↑(AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf a) a = ↑(Submodule.quotEquivOfEq (LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a)) (Ideal.span {↑(addOrderOf a)}) (_ : LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a) = Ideal.span {↑(addOrderOf a)})) (↑(LinearEquiv.symm (LinearMap.quotKerEquivRange (LinearMap.toSpanSingleton ℤ (↑A_) a))) (↑(LinearEquiv.ofEq (Submodule.span ℤ {a}) (LinearMap.range (LinearMap.toSpanSingleton ℤ (↑A_) a)) (_ : Submodule.span ℤ {a} = LinearMap.range (LinearMap.toSpanSingleton ℤ (↑A_) a))) a))

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf_symm_apply_coe {A_ : AddCommGroupCat} (a : ↑A_) : ∀ (a : ℤ ⧸ Ideal.span {↑(addOrderOf a)}), ↑(↑(LinearEquiv.symm (AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf a)) a) = ↑(↑↑(LinearEquiv.trans (LinearEquiv.symm (Submodule.quotEquivOfEq (LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a)) (Ideal.span {↑(addOrderOf a)}) (_ : LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a) = Ideal.span {↑(addOrderOf a)}))) (LinearMap.quotKerEquivRange (LinearMap.toSpanSingleton ℤ (↑A_) a))) a)

noncomputable def AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf {A_ : AddCommGroupCat} (a : ↑A_) : { x // x ∈ Submodule.span ℤ {a} } ≃ₗ[ℤ] ℤ ⧸ Ideal.span {↑(addOrderOf a)}

ℤ ⧸ ⟨ord(a)⟩ ≃ aℤ

theorem AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf_apply_self {A_ : AddCommGroupCat} (a : ↑A_) : ↑(AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf a) { val := a, property := (_ : a ∈ Submodule.span ℤ {a}) } = Submodule.Quotient.mk 1

@[inline, reducible]

abbrev AddCommGroupCat.enough_injectives_aux_proofs.divBy (n : ℕ) : ℤ →ₗ[ℤ] AddCircle 1

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

theorem AddCommGroupCat.enough_injectives_aux_proofs.divBy_self (n : ℕ) : ↑(AddCommGroupCat.enough_injectives_aux_proofs.divBy n) ↑n = 0

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle_apply {A_ : AddCommGroupCat} {a : ↑A_} : ∀ (a : { x // x ∈ Submodule.span ℤ {a} }), ↑AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle a = ↑(Submodule.liftQSpanSingleton (↑(addOrderOf a)) (AddCommGroupCat.enough_injectives_aux_proofs.divBy (if addOrderOf a = 0 then 2 else addOrderOf a)) (_ : ↑(AddCommGroupCat.enough_injectives_aux_proofs.divBy (if addOrderOf a = 0 then 2 else addOrderOf a)) ↑(addOrderOf a) = 0)) (↑(Submodule.quotEquivOfEq (LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a)) (Ideal.span {↑(addOrderOf a)}) (_ : LinearMap.ker (LinearMap.toSpanSingleton ℤ (↑A_) a) = Ideal.span {↑(addOrderOf a)})) (↑(LinearEquiv.symm (LinearMap.quotKerEquivRange (LinearMap.toSpanSingleton ℤ (↑A_) a))) (↑(LinearEquiv.ofEq (Submodule.span ℤ {a}) (LinearMap.range (LinearMap.toSpanSingleton ℤ (↑A_) a)) (_ : Submodule.span ℤ {a} = LinearMap.range (LinearMap.toSpanSingleton ℤ (↑A_) a))) a)))

noncomputable def AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle {A_ : AddCommGroupCat} {a : ↑A_} : { x // x ∈ Submodule.span ℤ {a} } →ₗ[ℤ] AddCircle 1

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

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 ∈ Submodule.span ℤ {a}) } = 0) : a = 0

theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_inj (A_ : AddCommGroupCat) : Function.Injective ↑(AddCommGroupCat.enough_injectives_aux_proofs.toNext A_)

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.presentation_J (A_ : AddCommGroupCat) : (AddCommGroupCat.enough_injectives_aux_proofs.presentation A_).J = AddCommGroupCat.enough_injectives_aux_proofs.next A_

@[simp]

theorem AddCommGroupCat.enough_injectives_aux_proofs.presentation_f (A_ : AddCommGroupCat) : (AddCommGroupCat.enough_injectives_aux_proofs.presentation A_).f = AddCommGroupCat.enough_injectives_aux_proofs.toNext A_

def AddCommGroupCat.enough_injectives_aux_proofs.presentation (A_ : AddCommGroupCat) : CategoryTheory.InjectivePresentation A_

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

instance AddCommGroupCat.enoughInjectives : CategoryTheory.EnoughInjectives AddCommGroupCat