res_obj_ρ — Mathlib

English

Let f: G →* H be a monoid hom and A a representation of H. Then the restricted representation (Action.res _ f).obj A has action ρ such that ρ(g) = A.ρ(f(g)) for all g ∈ G.

Русский

Пусть f: G →* H — гомоморфизм моноидов и A — представление H. Тогда ограниченное представление (Action.res _ f).obj A имеет действие ρ такое, что ρ(g) = A.ρ(f(g)) для всех g ∈ G.

LaTeX

$$$\rho_{(\mathrm{Res}_f A)}(g) = A.\rho(f(g))\quad(\text{для всех } g\in G)$$$

Lean4

@[simp]
theorem res_obj_ρ {H : Type u} [Monoid H] (f : G →* H) (A : Rep k H) : ρ ((Action.res _ f).obj A) = A.ρ.comp f :=
  rfl

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