of_iso_comparison — Mathlib

English

If the equalizer comparison map is an isomorphism, then G preserves the equalizer (limit).

Русский

Если равнопроизводитель равенств — изоморфизм, тогда G сохраняет равнопроизводитель (предел).

LaTeX

$$$[i : IsIso(\\text{equalizerComparison } f g G)] \\Rightarrow \\text{PreservesLimit}(\\text{parallelPair } f g, G)$$$

Lean4

/-- If the coequalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
coequalizer of `(f,g)`.
-/
theorem of_iso_comparison [i : IsIso (coequalizerComparison f g G)] : PreservesColimit (parallelPair f g) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)
  apply (isColimitMapCoconeCoforkEquiv _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (parallelPair (G.map f) (G.map g))) i

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