English
The construction A ↦ Ind_φ(A) defines a functor Rep_k(G) → Rep_k(H) sending each G-representation to its induced H-representation and each morphism to the induced morphism.
Русский
Конструкция A ↦ Ind_φ(A) определяет функтор Rep_k(G) → Rep_k(H), отправляющий каждое G-представление в индуцированное H-представление и каждое отображение в индуцированное отображение.
LaTeX
$$$$\mathrm{Ind}_\phi: \mathrm{Rep}_k(G) \to \mathrm{Rep}_k(H), \quad A \mapsto \mathrm{Ind}_\phi(A), \ f \mapsto \mathrm{ind}_\phi(f).$$$$
Lean4
/-- Given a group homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
to the induced `H`-representation `ind φ A`, with action on maps induced by left tensoring. -/
@[simps obj map]
noncomputable def indFunctor : Rep k G ⥤ Rep k H
where
obj A := ind φ A
map f := indMap φ f
map_id _ := by ext; rfl
map_comp _ _ := by ext; rfl
