preservesFiniteLimits_of_preservesKernels

English

If kernels are preserved, then all finite limits are preserved by the functor.

Русский

Если функтор сохраняет ядра, тогда он сохраняет все конечные пределы.

LaTeX

$$PreservesFiniteLimits F$$

Lean4

/-- A functor between preadditive categories which preserves kernels preserves all finite limits.
-/
theorem preservesFiniteLimits_of_preservesKernels [HasFiniteProducts C] [HasEqualizers C] [HasZeroObject C]
    [HasZeroObject D] [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] : PreservesFiniteLimits F :=
  have := preservesEqualizers_of_preservesKernels F
  have := preservesTerminalObject_of_preservesZeroMorphisms F
  have := preservesLimitsOfShape_pempty_of_preservesTerminal F
  have : PreservesFiniteProducts F := .of_preserves_binary_and_terminal F
  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts F

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