eHomEquiv_id

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.eHomEquiv_id

English

For any X, eHomEquiv_V maps id_X to eId_V X.

Русский

Для любого X биекция eHomEquiv_V отправляет id_X в eId_V X.

LaTeX

$$$eHomEquiv\,V\,(\mathrm{Id}\,X) = eId\,V\,X.$$$

Lean4

@[simp]
theorem eHomEquiv_id (X : C) : eHomEquiv V (𝟙 X) = eId V X :=
  EnrichedOrdinaryCategory.homEquiv_id _

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

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

Разделы

Аффилиация

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