English
The property of being injective as an R-module is equivalent to being injective as an object of the module category: ModuleCat.of(R, M) is injective iff M is injective as an R-module.
Русский
Свойство инъективности как R-модуля эквивалентно тому, что соответствующий объект в категории модулей инъективен: ModuleCat.of(R, M) инъективен тогда и только тогда, когда M — инъективный R-модуль.
LaTeX
$$$$ \\text{Module.Injective } R M \\;\\Longleftrightarrow\\; \\text{CategoryTheory.Injective}(\\text{ModuleCat.of } R M) $$$$
Lean4
theorem injective_module_of_injective_object [inj : CategoryTheory.Injective <| ModuleCat.of R M] : Module.Injective R M
where
out X Y _ _ _ _ f hf
g := by
have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
obtain rfl := ModuleCat.hom_ext_iff.mp h
exact ⟨l.hom, fun _ => rfl⟩
