ulift_injective_of_injective — Mathlib

English

If R is a ring and M is an additive abelian group, then the ULift of M, viewed as an R-module, is injective in ModuleCat.R.

Русский

Если R — кольцо, а M — аддитивная абелова группа, то ULift(M) с модулевой структурой над R является инъективным в ModuleCat(R).

LaTeX

$$$$ \\text{ModuleCat.ulift, injective}(R, M) $$$$

Lean4

instance ulift_injective_of_injective.{v'} [Small.{v} R] [AddCommGroup M] [Module R M]
    [CategoryTheory.Injective <| ModuleCat.of R M] : CategoryTheory.Injective <| ModuleCat.of R (ULift.{v'} M) :=
  Module.injective_object_of_injective_module (inj :=
    Module.ulift_injective_of_injective (inj := Module.injective_module_of_injective_object _ _))

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