instIsLeftAdjointTensorLeft

Mathlib.CategoryTheory.Closed.Types

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

English

For every type X, the functor tensorLeft X is a left adjoint.

Русский

Для каждого типа X функтор tensorLeft X является левым адъюнктом.

LaTeX

$$$ (\text{tensorLeft}(X)).IsLeftAdjoint $$$

Lean4

instance (X : Type v₁) : (tensorLeft X).IsLeftAdjoint :=
  ⟨_, ⟨Types.tensorProductAdjunction X⟩⟩

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

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

Разделы

Аффилиация

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