sumSMulInv_single_id — Mathlib

English

Given X ∈ FDRep k G and v ∈ X.V, there is a morphism rightFDRep ⟶ X whose underlying map is sumSMulInv v, i.e., the morphism from the right-regular representation to X sending the identity vector to v.

Русский

Для X ∈ FDRep k G и v ∈ X.V существует морфизм rightFDRep ⟶ X, чей базовый отображение равно сумме smul по v; он отправляет единичный вектор в v.

LaTeX

$$$\text{ofRightFDRep } (X,v) : rightFDRep \to X, \; \text{hom} = sumSMulInv v$ и др. соответствие коммутирует сρ.$$

Lean4

theorem sumSMulInv_single_id [Fintype G] [DecidableEq G] {X : FDRep k G} (v : X) :
    ∑ s : G, (single 1 1 : G → k) s • (X.ρ s⁻¹) v = v := by simp

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