instEnoughInjectivesModuleCatOfSmall

English

Let R be a ring and R be small. Then the category of R-modules has enough injectives: every R-module can be embedded into an injective R-module.

Русский

Пусть R — кольцо и рассматривается малое по базовой вселенной. Тогда категория модулей над R имеет достаточно инъективных объектов: каждый R-модуль можно вложить в инъективный R-модуль.

LaTeX

$$$\\forall M$, $\\exists E$ and $i: M \\to E$ such that $E$ is injective and $i$ is mono.$$

Lean4

instance [Small.{v} R] : EnoughInjectives (ModuleCat.{v} R) :=
  letI := enoughInjectives.{v} (Shrink.{v} R)
  EnoughInjectives.of_equivalence (restrictScalars (equivShrink R).symm.ringEquiv.toRingHom)

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