instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype

English

The coinduction functor is left adjoint to the restriction functor, hence it provides a left adjoint structure in the finite-index setting.

Русский

Коиндукционный функтор является левым сопряжённым к ограничению в случае конечного индекса.

LaTeX

$$$ \text{Coind}_S^G \dashv \mathrm{Res}_{S}^{G} \quad\text{in the finite-index setting}$$$

Lean4

noncomputable instance : (coindFunctor k S.subtype).IsLeftAdjoint :=
  (coindResAdjunction k S).isLeftAdjoint

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