instAdditiveInverse

Mathlib.CategoryTheory.Abelian.Transfer

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

English

The additive structure on the inverse of C induced by the equivalence is defined (Additive instance).

Русский

Наоборотный объект C через эквивалентность наследует аддитивную структуру.

LaTeX

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

Lean4

instance : (inverse C).Additive :=
  (equivalence C).symm.fullyFaithfulFunctor.additive_ofFullyFaithful

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

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

Разделы

Аффилиация

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