preservesSplitCoequalizers — Mathlib

English

If f,g admit a split coequalizer, then any functor G preserves the colimit of the parallel pair f,g.

Русский

Если пара стрелок f,g имеет разделяемый коэквалайзер, то любой функтор G сохраняет колимит параллельной пары f,g.

LaTeX

$$$\\text{HasSplitCoequalizer}(f,g) \\quad \\Rightarrow \\quad \\operatorname{PreservesColimit}(\\operatorname{parallelPair}(f,g), G).$$$

Lean4

/-- Any functor preserves coequalizers of split pairs. -/
instance (priority := 1) preservesSplitCoequalizers (f g : X ⟶ Y) [HasSplitCoequalizer f g] :
    PreservesColimit (parallelPair f g) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer
  apply (isColimitMapCoconeCoforkEquiv G _).symm ((HasSplitCoequalizer.isSplitCoequalizer f g).map G).isCoequalizer

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