English
Let φ: G → H be a group homomorphism and A a G-representation. The induced H-representation Ind_φ(A) is constructed on the H-module structure of k[H] ⊗_k A by letting H act via h · (h1 ⊗ a) = h1 h^{-1} ⊗ a, and then taking G-coinvariants. Equivalently, Ind_φ(A) is the representation Rep.of (A.ρ.ind φ).
Русский
Пусть φ: G → H — гомоморфизм групп, а A — представление над G. Индукированное по φ представление Ind_φ(A) строится на модуле k[H] ⊗_k A, где H действует так, что h · (h1 ⊗ a) = h1 h^{-1} ⊗ a, затем берутся G-коинварианты. Эквивалентно Ind_φ(A) = Rep.of (A.ρ.ind φ).
LaTeX
$$$\mathrm{Ind}_\phi A = \big(k[H] \otimes_k A\big)_G , \quad h \cdot \overline{h_1 \otimes a} = \overline{h_1 h^{-1} \otimes a}. $$$$
Lean4
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `A`, this is
`(k[H] ⊗[k] A)_G` equipped with the `H`-representation defined by sending `h : H` and `⟦h₁ ⊗ₜ a⟧`
to `⟦h₁h⁻¹ ⊗ₜ a⟧`. -/
noncomputable abbrev ind : Rep k H :=
Rep.of (A.ρ.ind φ)
