English
Let g be a group element. If π: W → V is a k-linear map between G-modules with a compatible MonoidAlgebra action, the g-conjugate of π is the map sending w ∈ W to g⁻¹ acting on V after applying π to g acting on w; i.e., π^g = g⁻¹ • π • g •.
Русский
Пусть g ∈ G. Пусть π: W → V — k-линейное отображение между модулями с действием G; конъюгированное отображение по g определяется как π^g = g⁻¹ • π • g •, то есть π^g(w) = g⁻¹ · π(g · w).
LaTeX
$$$\pi^{g} : W \to V \\ (\pi^{g})(w) = g^{-1} \cdot (\pi(g \cdot w))$$$
Lean4
/-- We define the conjugate of `π` by `g`, as a `k`-linear map. -/
def conjugate (g : G) : W →ₗ[k] V :=
GroupSMul.linearMap k V g⁻¹ ∘ₗ π ∘ₗ GroupSMul.linearMap k W g
