injective_as_module_iff — Mathlib

English

For an abelian group A, Injective(ModuleCat.of ℤ A)) is equivalent to Injective(AddCommGrpCat.of A) under the forgetful equivalence between ModuleCat and AddCommGrpCat.

Русский

Для абелевой группы A инъективность модуля над ℤ эквивалентна инъективности в AddCommGrpCat через забывающую эквивалентность между ModuleCat и AddCommGrpCat.

LaTeX

$$$ \\mathrm{Injective}(\\mathrm{ModuleCat.of} \\mathbb{Z} A) \\iff \\mathrm{Injective}(\\mathrm{AddCommGrpCat.of} A) $$$

Lean4

theorem injective_as_module_iff : Injective (ModuleCat.of ℤ A) ↔ Injective (C := AddCommGrpCat) (AddCommGrpCat.of A) :=
  ((forget₂ (ModuleCat ℤ) AddCommGrpCat).asEquivalence.map_injective_iff (ModuleCat.of ℤ A)).symm

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