of_iso_comparison — Mathlib

English

The equivalence between IsColimit for Functor.mapCocone of a Cofan.mk and IsColimit for Cofan.mk under G.

Русский

Эквиваленция IsColimit между Functor.mapCocone от Cofan.mk и IsColimit для Cofan.mk под G.

LaTeX

$$$\text{IsColimit}(\mathrm{Functor.mapCocone}\ G\ (\mathrm{Cofan.mk}\ P\ g)) \simeq \text{IsColimit}(\mathrm{Cofan.mk}\ (G\cdot P)\ (\lambda j. G.map (g\, j)))$$$

Lean4

/-- If `pi_comparison G f` is an isomorphism, then `G` preserves the limit of `f`. -/
theorem of_iso_comparison [i : IsIso (piComparison G f)] : PreservesLimit (Discrete.functor f) G :=
  by
  apply preservesLimit_of_preserves_limit_cone (productIsProduct f)
  apply (isLimitMapConeFanMkEquiv _ _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

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