enoughInjectives — Mathlib

English

For any ring R, the category of R-modules has enough injectives, via an adjunction between restriction and co-extension of scalars with ℤ.

Русский

Для кольца R категория R-модулей обладает достаточным количеством инъективных объектов, через сопряжённость ограничений и корасширения скаляров с ℤ.

LaTeX

$$$\text{EnoughInjectives}(\text{ModuleCat } R)$$$

Lean4

theorem enoughInjectives : EnoughInjectives (ModuleCat.{max v u} R) :=
  EnoughInjectives.of_adjunction (ModuleCat.restrictCoextendScalarsAdj.{max v u} (algebraMap ℤ R))

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