instAdditiveFunctor

Mathlib.CategoryTheory.Abelian.Transfer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShrinkHoms.instAdditiveFunctor

English

The functor ShrinkHoms.functor C is additive.

Русский

Функтор ShrinkHoms.functor C аддитивен.

LaTeX

$$$(\text{ShrinkHoms.functor } C).Additive$$$

Lean4

instance : (functor C).Additive :=
  (equivalence C).symm.additive_inverse_of_FullyFaithful

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

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

Разделы

Аффилиация

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