isLeftAdjoint_inverse

Mathlib.CategoryTheory.Adjunction.Basic

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

English

A variant stating that e.inverse is left adjoint to e.functor in the equivalence e: C ≌ D.

Русский

Вариант утверждения, что e.inverse является левой adjoint к e.functor в эквивалентности e: C ≌ D.

LaTeX

$$$ e^{-1} \dashv e. functor $$$

Lean4

theorem isLeftAdjoint_inverse : e.inverse.IsLeftAdjoint :=
  e.symm.isLeftAdjoint_functor

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

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

Разделы

Аффилиация

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