English
For h1,h2 in H and a in A, IndV.mk φ ρ h1 (IndV.mk φ ρ h2 a) = IndV.mk φ ρ (h2 h1^{-1}) a.
Русский
Для h1,h2 ∈ H и a ∈ A, выполняется формула IndV.mk φ ρ h1 (IndV.mk φ ρ h2 a) = IndV.mk φ ρ (h2 h1^{-1}) a.
LaTeX
$$$\\mathrm{IndV.mk}\\; φ\\; ρ\\; h_1 \\big( \\mathrm{IndV.mk}\\; φ\\; ρ\\; h_2\\; a \\big) = \\mathrm{IndV.mk}\\; φ\\; ρ\\; (h_2 h_1^{-1})\\; a$$$
Lean4
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
`k`-module `(k[H] ⊗[k] A)_G` with the `G`-representation on `k[H]` defined by `φ`.
See `Representation.ind` for the induced `H`-representation on `IndV φ ρ`. -/
abbrev IndV :=
Coinvariants (V := TensorProduct k (H →₀ k) A) (Representation.tprod ((leftRegular k H).comp φ) ρ)
