instIsLeftAdjointDiscreteTensorLeftCompIncl

English

For any discrete index I and a functor F : I ⥤ C, the functor tensorLeft ((incl ✝ I) ∘ F) is left adjoint.

Русский

Для дискретного индекса I и функторы F: I ⥤ C, отображение tensorLeft ((incl ✝ I) ∘ F) является левым сопряжённым.

LaTeX

$$$ \\text{IsLeftAdjoint} \\left( \\mathrm{tensorLeft} \\left( (\\mathrm{incl✝ I}) \\cdot F \\right) \\right)$$$

Lean4

instance (F : I ⥤ C) : IsLeftAdjoint (tensorLeft (incl I ⋙ F)) :=
  (ihom.adjunction (incl I ⋙ F)).isLeftAdjoint

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