instHasKernelToSubtype

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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

English

There exists a cokernel for biproduct.fromSubtype f p in the finite/biproduct context.

Русский

Существует коконцентр biproduct.fromSubtype f p в контексте конечной/биопродуктной структуры.

LaTeX

$$$\\text{HasCokernel}(\\text{biproduct.fromSubtype } f p)$$$

Lean4

instance (p : Set K) : HasKernel (biproduct.toSubtype f p) :=
  HasLimit.mk (kernelForkBiproductToSubtype f p)

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

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

Разделы

Аффилиация

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