English
The coinduction construction extends to a functor sending a G-representation to its coinduced H-representation along φ, with action on maps by coindMap.
Русский
Операция коиндукции расширяется до функторa, отправляющего G-представление в коиндудированное H-представление по φ, действующего на отображения через coindMap.
LaTeX
$$$\mathrm{Rep}_{k}G \xrightarrow{\mathrm{coind}_{\phi}} \mathrm{Rep}_{k}H.$$$
Lean4
/-- Given a monoid homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
to the coinduced `H`-representation `coind φ A`, with action on maps given by postcomposition. -/
@[simps obj map]
noncomputable def coindFunctor : Rep k G ⥤ Rep k H
where
obj A := coind φ A
map f := coindMap φ f
