ρ_hom — Mathlib

English

For any g ∈ G, the hom component of the action on X matches the underlying morphism X.ρ g; i.e., the action morphism equals the corresponding MonoidHom component.

Русский

Пусть для каждого g ∈ G выполняется: ρ_hom гом-часть действия на X совпадает с отображением X.ρ g; то есть действие на X по g задаётся через соответствующий компонент MonoidHom.

LaTeX

$$$ (\mathrm{Action.\} \rho X\; g).\hom = X.\rho g $$$

Lean4

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

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