injective_of_divisible — Mathlib

English

If A is divisible, then AddCommGrpCat.of A is an injective object in AddCommGrpCat.

Русский

Если A делимо, то объект AddCommGrpCat.of A является инъективным в AddCommGrpCat.

LaTeX

$$$ [\\text{DivisibleBy } A \\mathbb{Z}] \\Rightarrow \\mathrm{Injective}(\\mathrm{AddCommGrpCat.of} A) $$$

Lean4

instance injective_of_divisible [DivisibleBy A ℤ] : Injective (C := AddCommGrpCat) (AddCommGrpCat.of A) :=
  (injective_as_module_iff A).mp <|
    Module.injective_object_of_injective_module (inj := (Module.Baer.of_divisible A).injective)

Похожие утверждения