instEnoughInjectivesModuleCatInt — Mathlib

English

The category of modules over the integers ℤ has enough injectives, via the forgetful functor to AddCommGrp.

Русский

Категория модулей над целыми числами ℤ обладает достаточными инъективами через забудьку к AddCommGrp.

LaTeX

$$$\text{EnoughInjectives } (ModuleCat \mathbb{Z})$$$

Lean4

instance : EnoughInjectives (ModuleCat.{v} ℤ) :=
  EnoughInjectives.of_equivalence (forget₂ (ModuleCat ℤ) AddCommGrpCat)

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