homAddEquiv_neg

Mathlib.CategoryTheory.Adjunction.Additive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.homAddEquiv_neg

English

Negation commutes with additive hom-equivalence.

Русский

Отрицание коммутирует с аддитивным сопоставлением гомоморфизмов.

LaTeX

$$$adj.homEquiv X Y (-f) = -adj.homEquiv X Y f$$$

Lean4

@[simp]
theorem homAddEquiv_neg (X : C) (Y : D) (f : F.obj X ⟶ Y) : adj.homEquiv X Y (-f) = -adj.homEquiv X Y f :=
  map_neg (adj.homAddEquiv X Y) _

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

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

Разделы

Аффилиация

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