isBilimitBinaryBiconeOfIsSplitEpiOfKernel

Mathlib.CategoryTheory.Preadditive.Biproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel

Lean4

/-- The bicone constructed in `binaryBiconeOfIsSplitEpiOfKernel` is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories. -/
def isBilimitBinaryBiconeOfIsSplitEpiOfKernel {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) :
    (binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit :=
  BinaryBicone.isBilimitOfKernelInl _ <| i.ofIsoLimit <| Fork.ext (Iso.refl _) (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru