hasEqualizer_of_hasKernel — Mathlib

English

If a preadditive category has a kernel of f − g, then it has an equalizer of f and g.

Русский

Пусть в преддобавительной категории существует ядро морфизма f − g; тогда существуют равнители f и g.

LaTeX

$$HasKernel(f - g) ⇒ HasEqualizer(f, g)$$

Lean4

/-- A preadditive category has an equalizer for `f` and `g` if it has a kernel for `f - g`. -/
theorem hasEqualizer_of_hasKernel [HasKernel (f - g)] : HasEqualizer f g :=
  HasLimit.mk
    { cone := forkOfKernelFork _
      isLimit := isLimitForkOfKernelFork (equalizerIsEqualizer (f - g) 0) }

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