isRightAdjoint_inverse

Mathlib.CategoryTheory.Adjunction.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.isRightAdjoint_inverse

English

For an equivalence e: C ≌ D, the inverse e.inverse is a right adjoint.

Русский

Для эквивалентности e: C ≌ D обратная e.inverse является правым adjoint.

LaTeX

$$$ e^{-1} \text{ is right adjoint to } e. tofunctor $$$

Lean4

theorem isRightAdjoint_inverse : e.inverse.IsRightAdjoint where exists_leftAdjoint := ⟨_, ⟨e.toAdjunction⟩⟩

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

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

Разделы

Аффилиация

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