English
Let i: V ≅ W be an isomorphism of representations. Then the action maps ρ on W are obtained from those on V by conjugation with the linear equivalence associated to i. In particular, for every g ∈ G, W.ρ(g) is the conjugate of V.ρ(g) by the isomorphism i.
Русский
Пусть i: V ≅ W является изоморфизмом представлений. Тогда действия ρ на W получаются из действий на V конъюгацией по линейному эквиваленту, соответствующему i. Для каждого g ∈ G выполняется W.ρ(g) = i^{-1} V.ρ(g) i.
LaTeX
$$$W.\rho g = (FDRep.isoToLinearEquiv i).conj\ (V.\rho g)$$$
Lean4
theorem conj_ρ {V W : FDRep R G} (i : V ≅ W) (g : G) : W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g) :=
by
rw [FDRep.isoToLinearEquiv, ← hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj, Iso.conj_apply, ←
ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff, Iso.eq_inv_comp ((Action.forget (FGModuleCat R) G).mapIso i)]
exact (i.hom.comm g).symm
