preservesSplitEqualizers — Mathlib

English

If f,g admit a split equalizer, then G preserves the limit of the parallel pair f,g.

Русский

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

LaTeX

$$$\\text{HasSplitEqualizer}(f,g) \\Rightarrow \\operatorname{PreservesLimit}(\\operatorname{parallelPair}(f,g), G).$$$

Lean4

instance (priority := 1) preservesSplitEqualizers (f g : X ⟶ Y) [HasSplitEqualizer f g] :
    PreservesLimit (parallelPair f g) G :=
  by
  apply preservesLimit_of_preserves_limit_cone (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer
  apply (isLimitMapConeForkEquiv G _).symm ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer

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