English
There is a natural adjunction between the coinvariants functor and the trivial representation functor: coinvariants k G ⊣ trivial k G.
Русский
Существует естественная adjunction между функтором coinvariants и тривиальным функтором представления: coinvariants k G ⊣ trivial k G.
LaTeX
$$$\mathrm{coinvariantsFunctor}_{k,G} \dashv \mathrm{trivialFunctor}_{k,G}$$$
Lean4
/-- The adjunction between the functor sending a representation to its coinvariants and the functor
equipping a module with the trivial representation. -/
@[simps]
noncomputable def coinvariantsAdjunction : coinvariantsFunctor k G ⊣ trivialFunctor k G
where
unit :=
{
app
X :=
{ hom := (coinvariantsMk k G).app X
comm _ := by ext; simp [ModuleCat.endRingEquiv, trivialFunctor] } }
counit := { app X := desc (B := trivial k G X) (𝟙 _) }
