English
If f: A → B is a morphism of G-representations, then Ind_φ(f): Ind_φ(A) → Ind_φ(B) is the induced morphism of H-representations, constructed by tensoring with the Monoid algebra and applying f on the A-factor.
Русский
Если f: A → B — гомоморфизмRepresentations G, то Ind_φ(f): Ind_φ(A) → Ind_φ(B) есть индуцированное отображение между H-представлениями, получаемое тензоризацией с k[H] и применением f к A-компоненте.
LaTeX
$$$$\mathrm{Ind}_\phi(f): \mathrm{Ind}_\phi(A) \to \mathrm{Ind}_\phi(B), \quad \overline{h \otimes a} \mapsto \overline{h \otimes f(a)}.$$$$
Lean4
/-- Given a group homomorphism `φ : G →* H`, a morphism of `G`-representations `f : A ⟶ B` induces
a morphism of `H`-representations `(k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G`. -/
@[simps]
noncomputable def indMap {A B : Rep k G} (f : A ⟶ B) : ind φ A ⟶ ind φ B
where
hom :=
ModuleCat.ofHom <|
Representation.Coinvariants.map _ _ (LinearMap.lTensor (H →₀ k) f.hom.hom) fun g => by ext; simp [hom_comm_apply]
comm
_ := by
ext
simp [ModuleCat.endRingEquiv]
