English
Compatibility of IndV.mk with the induced representation: matches the action of H on A.
Русский
Совместимость IndV.mk с индуцированным представлением: совпадает с действием H на A.
LaTeX
$$IndV.mk φ ρ (h₂ h₁^{-1}) a = (IndV.mk φ ρ h₁)(IndV.mk φ ρ h₂ 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⟧`. -/
@[simps]
noncomputable def ind : Representation k H (IndV φ ρ)
where
toFun h := Coinvariants.map _ _ ((lmapDomain k k fun x => x * h⁻¹).rTensor _) fun _ => by ext; simp [mul_assoc]
map_one' := by ext; simp
map_mul' _ _ := by ext; simp [IndV, mul_assoc]
