conjugate_apply — Mathlib

English

Fix a finite group G and a field k. For a given π: W → V, the g-conjugate π^g evaluated at v ∈ W equals the scalar monomial corresponding to g⁻¹ via the group algebra acting on V, applied to π of the g-action on v.

Русский

Пусть G конечна, k — тело. Для отображения π: W → V выполняется: (π^g)(v) = MonoidAlgebra.single g⁻¹ (1) • π(MonoidAlgebra.single g (1) • v).

LaTeX

$$$ (\pi^{g})(v) = \ MonoidAlgebra.single\ g^{-1} (1 : k) \; \cdot \; π(\ MonoidAlgebra.single\ g (1 : k) \cdot v)$$$

Lean4

theorem conjugate_apply (g : G) (v : W) :
    π.conjugate g v = MonoidAlgebra.single g⁻¹ (1 : k) • π (MonoidAlgebra.single g (1 : k) • v) :=
  rfl

Похожие утверждения