coindFunctor' — Mathlib

English

There is a functor Rep.k G ⥤ Rep k H giving the coinduction along φ, with object map A ↦ coind' φ A and morphisms mapped by coindMap'.

Русский

Существует функтор Rep_k G ⥤ Rep_k H, задающий коиндукцию вдоль φ: A ↦ коинд' φ A, а отображения переводятся через coindMap'.

LaTeX

$$$\mathrm{Rep}_{k}G \xrightarrow{\mathrm{coind}'} \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

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