instIsLeftAdjointLeftAdjoint — Mathlib

English

If R is a right adjoint, then its left adjoint R.leftAdjoint is indeed a left adjoint.

Русский

Если R является правым сопряжённым, то левый сопряжённый R.leftAdjoint действительно является левым сопряжённым.

LaTeX

$$$\text{If } (R : D \to C) \text{ isRightAdjoint}, \; R.leftAdjoint \text{ isLeftAdjoint}$$$

Lean4

instance (R : D ⥤ C) [R.IsRightAdjoint] : R.leftAdjoint.IsLeftAdjoint :=
  (ofIsRightAdjoint R).isLeftAdjoint

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