homEquiv_symm_id

Mathlib.CategoryTheory.Adjunction.Basic

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

English

The inverse bijection sends the identity on G X to the counit at X.

Русский

Обратная биекция переводит тождественный комплекс на G X вCounit на X.

LaTeX

$$$\forall X,\; (\mathrm{homEquiv}\; (G.obj X) X)^{-1}(\mathrm{Id}_{G X}) = \mathrm{counit}_{X}$$$

Lean4

theorem homEquiv_symm_id (X : D) : (adj.homEquiv _ X).symm (𝟙 _) = adj.counit.app X := by simp

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

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

Разделы

Аффилиация

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