instIsLeftAdjointModuleCatCoinvariantsFunctor

English

The coinvariants functor is a left adjoint to its right adjoint (the adjunction between coinvariants and trivial functor).

Русский

Функтор монопредставлений является левым сопряженным к своему правому сопряженному функтору (сопоставление монопредставлений и тривиального функторного сопряжения).

LaTeX

$$$\\text{IsLeftAdjoint} (\\text{coinvariantsFunctor } k G)$$$

Lean4

instance : (coinvariantsFunctor k G).IsLeftAdjoint :=
  (coinvariantsAdjunction k G).isLeftAdjoint

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