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 (written additively) has enough injectives.
• CommGroupCat.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 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)

Equations

• (_ : CategoryTheory.Injective (CategoryTheory.Bundled.mk A)) = (_ : CategoryTheory.Injective (CategoryTheory.Bundled.mk A))

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

Equations

• AddCommGroupCat.injective_ratCircle = (_ : CategoryTheory.Injective (CategoryTheory.Bundled.mk (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 →+ ℚ/ℤ}, ℚ/ℤ.

Equations

• AddCommGroupCat.enough_injectives_aux_proofs.next A_ = AddCommGroupCat.of ((A_ ⟶ AddCommGroupCat.of (ULift.{u, 0} (AddCircle 1))) → ULift.{u, 0} (AddCircle 1))

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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_1 : ↥(Submodule.span ℤ {a})), (AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf a) a_1 = (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_1))

@[simp]

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

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

ℤ ⧸ ⟨ord(a)⟩ ≃ aℤ

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• AddCommGroupCat.enough_injectives_aux_proofs.divBy n = LinearMap.toSpanSingleton ℤ (AddCircle 1) ↑(↑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_1 : ↥(Submodule.span ℤ {a})), AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle a_1 = (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_1)))

noncomputable def AddCommGroupCat.enough_injectives_aux_proofs.toRatCircle {A_ : AddCommGroupCat} {a : ↑A_} : ↥(Submodule.span ℤ {a}) →ₗ[ℤ] AddCircle 1

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

Equations

• One or more equations did not get rendered due to their size.

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 →+ ℚ/ℤ}, ℚ/ℤ.

Equations

• One or more equations did not get rendered due to their size.

instance AddCommGroupCat.enoughInjectives : CategoryTheory.EnoughInjectives AddCommGroupCat

Equations

• AddCommGroupCat.enoughInjectives = (_ : CategoryTheory.EnoughInjectives AddCommGroupCat)

instance CommGroupCat.enoughInjectives : CategoryTheory.EnoughInjectives CommGroupCat

Equations

• CommGroupCat.enoughInjectives = (_ : CategoryTheory.EnoughInjectives CommGroupCat)