English
The lemma describes how an element g ∈ G acts on a linear map f ∈ V → W through the linHom representation: (linHom ρV ρW) g f = ρW g ∘ f ∘ ρV g^{-1}.
Русский
Лемма описывает, как элемент g группы действует на линейное отображение f через представление linHom: g действует через ρ_W(g) ∘ f ∘ ρ_V(g)^{-1}.
LaTeX
$$$ (linHom ρ_V ρ_W) g \\; f = ρ_W g \\circ f \\circ ρ_V g^{-1} $$$
Lean4
/-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on the
module `V →ₗ[k] W`, where `G` acts by conjugation.
-/
def linHom : Representation k G (V →ₗ[k] W)
where
toFun
g :=
{ toFun := fun f => ρW g ∘ₗ f ∘ₗ ρV g⁻¹
map_add' := fun f₁ f₂ => by simp_rw [add_comp, comp_add]
map_smul' := fun r f => by simp_rw [RingHom.id_apply, smul_comp, comp_smul] }
map_one' := ext fun x => by simp [Module.End.one_eq_id]
map_mul' g h := ext fun x => by simp [Module.End.mul_eq_comp, comp_assoc]
