coe_res_obj_ρ — Mathlib

English

For any g ∈ G, A.hom, and restriction f: G →* H with A a representation of H, the evaluation of ρ on the restricted object satisfies (ρ((Action.res _ f).obj A)) (g) = A.ρ(f(g)).

Русский

Для любого g ∈ G верно, что (ρ(restriction)).(g) = A.ρ(f(g)).

LaTeX

$$$\rho_{(\mathrm{Res}_f A)}(g) = A.\rho(f(g))\quad(\forall g\in G)$$$

Lean4

@[simp]
theorem coe_res_obj_ρ {H : Type u} [Monoid H] (f : G →* H) (A : Rep k H) (g : G) :
    DFunLike.coe (F := G →* (A →ₗ[k] A)) (ρ ((Action.res _ f).obj A)) g = A.ρ (f g) :=
  rfl

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