English
A linear map f lies in invariants iff it commutes with the action of all g ∈ G on the source and target representations.
Русский
Линейное отображение f принадлежит инвариантам тогда и только тогда, когда оно commuting с действием всей группы.
LaTeX
$$$$ f \in \mathrm{invariants}\; X.\rho \to Y.\rho \iff \forall g \in G, f \circ X.\rho(g) = Y.\rho(g) \circ f. $$$$
Lean4
theorem mem_invariants_iff_comm {X Y : Rep k G} (f : X.V →ₗ[k] Y.V) (g : G) :
(linHom X.ρ Y.ρ) g f = f ↔ f.comp (X.ρ g) = (Y.ρ g).comp f :=
by
dsimp
rw [← LinearMap.comp_assoc, ← ModuleCat.hom_ofHom (Y.ρ g), ← ModuleCat.hom_ofHom f, ← ModuleCat.hom_comp, ←
ModuleCat.hom_ofHom (X.ρ g⁻¹), ← ModuleCat.hom_comp, Rep.ofHom_ρ, ← ρAut_apply_inv X g, Rep.ofHom_ρ, ←
ρAut_apply_hom Y g, ← ModuleCat.hom_ext_iff, Iso.inv_comp_eq, ρAut_apply_hom, ← ModuleCat.hom_ofHom (X.ρ g), ←
ModuleCat.hom_comp, ← ModuleCat.hom_ext_iff]
exact comm
