expComparison

Mathlib.CategoryTheory.Closed.Functor

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

Lean4

/-- The exponential comparison map.
`F` is a Cartesian-closed functor if this is an iso for all `A`.
-/
def expComparison (A : C) : TwoSquare (exp A) F F (exp (F.obj A)) :=
  mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)) (prodComparisonNatIso F A).inv

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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