English
The category AddCommGrpCat has enough injectives; in particular, there exists an injective presentation for each object constructed via the CharacterModule construction given in the instance.
Русский
У категории AddCommGrpCat достаточно внедряющих объектов (injectives); для каждого объекта существует внедряющее представление, задаваемое конструктором по данным в примере.
LaTeX
$$$ \text{EnoughInjectives AddCommGrpCat} $$$
Lean4
instance enoughInjectives : EnoughInjectives AddCommGrpCat.{u} where
presentation
A_ :=
Nonempty.intro
{ J := of <| (CharacterModule A_) → ULift.{u} (AddCircle (1 : ℚ))
injective := injective_of_divisible _
f := ofHom ⟨⟨fun a i ↦ ULift.up (i a), by aesop⟩, by aesop⟩
mono :=
(AddCommGrpCat.mono_iff_injective _).mpr <|
(injective_iff_map_eq_zero _).mpr fun _ h0 ↦
eq_zero_of_character_apply (congr_arg ULift.down <| congr_fun h0 ·) }
