of_iso_comparison — Mathlib

English

There is an equivalence of limits: IsLimit(G.mapCone(Fork.ofι h w)) ≃ IsLimit(Fork.ofι (G.map h) ...).

Русский

Существуют эквивалентности предельности: IsLimit(G.mapCone(Fork.ofι h w)) ≃ IsLimit(Fork.ofι(G.map h) ...).

LaTeX

$$$IsLimit\\big(G.mapCone(Fork.ofι\,h\,w)\\big) \\simeq IsLimit\\big(Fork.ofι(G.map\,h)\\big)$$$

Lean4

/-- If the equalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
equalizer of `(f,g)`.
-/
theorem of_iso_comparison [i : IsIso (equalizerComparison f g G)] : PreservesLimit (parallelPair f g) G :=
  by
  apply preservesLimit_of_preserves_limit_cone (equalizerIsEqualizer f g)
  apply (isLimitMapConeForkEquiv _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (parallelPair (G.map f) (G.map g))) i

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