ofHom_ρ — Mathlib

English

For any g ∈ G, the ModuleCat.ofHom (X.ρ g) agrees with the action ρ on X; i.e., the embedding of the endomorphism given by ρ g coincides with the action ρ g.

Русский

Для любого g ∈ G отображение ModuleCat.ofHom (X.ρ g) совпадает с действием ρ на X; то есть встроенная структура совпадает с действием ρ g.

LaTeX

$$$\mathrm{ModuleCat.ofHom} (X.\rho g) = \mathrm{Action.\} ρ X g$$$

Lean4

@[simp]
theorem ofHom_ρ {X : Rep k G} (g : G) : ModuleCat.ofHom (X.ρ g) = Action.ρ X g :=
  rfl

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