injective_object_of_injective_module

English

If M is an injective R-module, then the corresponding object ModuleCat.of(R, M) is injective in the category ModuleCat(R).

Русский

Если M является инъективным R-модулем, то соответствующий объект ModuleCat.of(R, M) является инъективным в категории ModuleCat(R).

LaTeX

$$$$ \\text{ModuleCat.of}(R, M) \\text{ is injective in } \\text{ModuleCat}(R) \\text{ whenever } M \\text{ is injective as an } R\\text{-module} $$$$

Lean4

theorem injective_object_of_injective_module [inj : Injective R M] : CategoryTheory.Injective (ModuleCat.of R M) where
  factors g f
    m :=
    have ⟨l, h⟩ := inj.out f.hom ((ModuleCat.mono_iff_injective f).mp m) g.hom
    ⟨ModuleCat.ofHom l, by ext x; simpa using h x⟩

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