preservesFiniteColimits_of_preservesCokernels

English

A functor between preadditive categories preserving kernels preserves all finite limits.

Русский

Функтор между прeдадитивными категориями, сохраняющий ядра, сохраняет все конечные пределы.

LaTeX

$$PreservesFiniteLimits (F)$$

Lean4

/-- A functor between preadditive categories which preserves kernels preserves all finite limits.
-/
theorem preservesFiniteColimits_of_preservesCokernels [HasFiniteCoproducts C] [HasCoequalizers C] [HasZeroObject C]
    [HasZeroObject D] [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] : PreservesFiniteColimits F :=
  by
  letI := preservesCoequalizers_of_preservesCokernels F
  letI := preservesInitialObject_of_preservesZeroMorphisms F
  letI := preservesColimitsOfShape_pempty_of_preservesInitial F
  letI : PreservesFiniteCoproducts F := ⟨fun _ ↦ preservesFiniteCoproductsOfPreservesBinaryAndInitial F _⟩
  exact preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

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