homAddEquiv_symm_zero

Mathlib.CategoryTheory.Adjunction.Additive

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

English

The symmetric hom-equivalence sends zero to zero.

Русский

Симметричное гомоэквивалентность отображает ноль в ноль.

LaTeX

$$$(adj.homEquiv X Y).symm 0 = 0$$$

Lean4

@[simp]
theorem homAddEquiv_symm_zero (X : C) (Y : D) : (adj.homEquiv X Y).symm 0 = 0 :=
  map_zero (adj.homAddEquiv X Y).symm

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

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

Разделы

Аффилиация

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