hasKernel_of_hasEqualizer — Mathlib

English

If f and g have an equalizer, then f − g has a kernel.

Русский

Если существуют равнители f и g, то f − g имеет ядро.

LaTeX

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

Lean4

/-- A preadditive category has a kernel for `f - g` if it has an equalizer for `f` and `g`. -/
theorem hasKernel_of_hasEqualizer [HasEqualizer f g] : HasKernel (f - g) :=
  HasLimit.mk
    { cone := kernelForkOfFork (equalizer.fork f g)
      isLimit := isLimitKernelForkOfFork (limit.isLimit (parallelPair f g)) }

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