instAdditiveKaroubiInverse

Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiInverse

English

The additive structure on Karoubi(C) has an additive inverse functor, provided C is Preadditive.

Русский

Аддитивная структура Karoubi(C) имеет аддитивный обратный функтор, если C предаддитивна.

LaTeX

$$$\text{inverse}_{\mathrm{Karoubi}}(C)$ Additive$$

Lean4

instance [Preadditive C] : Functor.Additive (inverse C) where

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

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

Разделы

Аффилиация

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