preservesCoequalizers_of_preservesCokernels

English

A functor that preserves kernels preserves all coequalizers.

Русский

Функтор, сохраняющий ядра, сохраняет все коэкваленты.

LaTeX

$$PreservesCoequalizers_of_preservesCokernels F$$

Lean4

/-- A functor between preadditive categories preserves all coequalizers if it preserves all kernels.
-/
theorem preservesCoequalizers_of_preservesCokernels [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] :
    PreservesColimitsOfShape WalkingParallelPair F where
  preservesColimit
    {K} :=
    by
    letI :=
      preservesCoequalizer_of_preservesCokernels F (K.map Limits.WalkingParallelPairHom.left)
        (K.map Limits.WalkingParallelPairHom.right)
    apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

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