of_iso_comparison — Mathlib

English

There is an isomorphism between IsLimit structures for mapped and mapped cones of kernels.

Русский

Существуют изоморфизмы пределов для отображённых и отображённых конусов ядер.

LaTeX

$$$IsLimitMapConeEquiv : IsLimit( G.mapCone c ) \\simeq IsLimit( c.map G )$$$

Lean4

/-- If the cokernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
cokernel of `f`.
-/
theorem of_iso_comparison [i : IsIso (cokernelComparison f G)] : PreservesColimit (parallelPair f 0) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
  apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (cokernelIsCokernel (G.map f)) i

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