isPullbackEquivIsLimitKernelFork — Mathlib

English

A commutative square in a preadditive category is a pullback square iff the induced diagram with the kernel is a kernel diagram.

Русский

Коммутативный квадрат в предадитивной категории является pullback- квадратом тогда и только тогда, когда диаграмма, индуцированная ядром, является диаграммой ядра.

LaTeX

$$$\\text{IsPullback}(sq) \\simeq \\text{IsLimit}(sq\\,\\text{kernelFork})$$$

Lean4

/-- A commutative square in a preadditive category is a pullback square iff
the corresponding diagram `0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₁` a kernel. -/
noncomputable def isPullbackEquivIsLimitKernelFork : sq.IsPullback ≃ IsLimit sq.kernelFork :=
  Equiv.trans
    { toFun := fun h ↦ h.isLimit
      invFun := fun h ↦ IsPullback.mk _ h
      right_inv := fun _ ↦ Subsingleton.elim _ _ } sq.commSq.isLimitEquivIsLimitKernelFork

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