leftRegularHomEquiv_symm_single — Mathlib

English

The free lift hom applied to a singleton basis corresponds to the action of ρ on the image of the index i, scaled by r.

Русский

Гомоморфизм freeLift, применённый к одиночке, соответствует действию ρ на образ индекса i, масштабированному коэффициентом r.

LaTeX

$$(\text{freeLift } A f).hom(\mathrm{single i (single g r)}) = r \cdot A.\rho(g) (f i)$$

Lean4

theorem leftRegularHomEquiv_symm_single {A : Rep k G} (x : A) (g : G) :
    ((leftRegularHomEquiv A).symm x).hom (Finsupp.single g 1) = A.ρ g x := by simp

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