English
The dual of a representation ρ of G on V is the representation on the dual module V^* defined by (dual ρ) g f = f ∘ ρV(g)^{-1} for f ∈ V^*.
Русский
Двойственное представление ρ на V — это представление на двойственном модуле V^*; действие g определяется как (dual ρ) g f = f ∘ ρV(g)^{-1}.
LaTeX
$$$ (dual ρ) g = f \\mapsto f \\circ ρ_V(g)^{-1} $ on V^*$$
Lean4
/-- The dual of a representation `ρ` of `G` on a module `V`, given by `(dual ρ) g f = f ∘ₗ (ρ g⁻¹)`,
where `f : Module.Dual k V`.
-/
def dual : Representation k G (Module.Dual k V)
where
toFun
g :=
{ toFun := fun f => f ∘ₗ ρV g⁻¹
map_add' := fun f₁ f₂ => by simp only [add_comp]
map_smul' := fun r f => by
ext
simp only [coe_comp, Function.comp_apply, smul_apply, RingHom.id_apply] }
map_one' := by ext; simp
map_mul' g h := by ext; simp
