hasKernels_moduleCat — Mathlib

English

For every morphism f in ModuleCat(R), there exists a kernel; i.e., the category has kernels.

Русский

Для каждого морфизма f в ModuleCat(R) существует ядро; категория имеет ядра.

LaTeX

$$$$ \\text{HasKernels}(\\mathrm{ModuleCat}(R)) $$$$

Lean4

/-- The category of R-modules has kernels, given by the inclusion of the kernel submodule. -/
theorem hasKernels_moduleCat : HasKernels (ModuleCat R) :=
  ⟨fun f => HasLimit.mk ⟨_, kernelIsLimit f⟩⟩

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