instHasCoequalizers — Mathlib

English

In the category of R-modules, coequalizers exist for every pair of parallel arrows. That is, given two morphisms between modules with the same domain and codomain, their coequalizer is present in Mod_R.

Русский

В категории R-модулей существуют ко-равномерения для любой пары параллельных отображений. Для любых двух гомоморфизмов между модулями их ко-равномерение существует в Mod_R.

LaTeX

$$$\\forall f,g: M \\rightrightarrows N, \\; \\exists \\operatorname{Coeq}(f,g) \\in \\mathrm{Mod}_R.$$$

Lean4

instance : HasCoequalizers (ModuleCat.{v} R) where

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