evaluationIsLeftAdjoint

Mathlib.CategoryTheory.Adjunction.Evaluation

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

English

If each costructured arrow category on G has a terminal object, G is a left adjoint.

Русский

Если в каждой CostructuredArrow G A существует терминальный объект, то G — левая адъюнктность.

LaTeX

$$∀ A HasTerminal(CostructuredArrow G A) ⇒ G.IsLeftAdjoint$$

Lean4

instance evaluationIsLeftAdjoint (c : C) : ((evaluation _ D).obj c).IsLeftAdjoint :=
  ⟨_, ⟨evaluationAdjunctionLeft _ _⟩⟩

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

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

Разделы

Аффилиация

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