of_iso_comparison — Mathlib

English

Similar to isColimitMapCoconeEquiv', but for kernels; the map of a kernel cone is a limit iff the mapped kernel cone is a limit.

Русский

Аналогично эквивалентности для кокон-кофора, но для ядер: отображение ядра коники является пределом тогда и только тогда, когда отображённый ядро-кофор — предел.

LaTeX

$$$\\text{isLimitMapConeEquiv'} : IsLimit (G.mapCone (KernelFork.ofι h w)) \\simeq IsLimit (KernelFork.ofι (G.map h) (by simp)) $$$

Lean4

/-- If the kernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
kernel of `f`.
-/
theorem of_iso_comparison [i : IsIso (kernelComparison f G)] : PreservesLimit (parallelPair f 0) G :=
  by
  apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
  apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (kernelIsKernel (G.map f)) i

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