hasCokernels_moduleCat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The category of R-modules has cokernels, given by the projection onto the quotient. -/
theorem hasCokernels_moduleCat : HasCokernels (ModuleCat R) :=
  ⟨fun f => HasColimit.mk ⟨_, cokernelIsColimit f⟩⟩

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