hom_comm_apply — Mathlib

English

For any morphism f: A ⟶ B and any g ∈ G, the action commutes with f; i.e., f.hom intertwines the G-actions: f.hom(A.ρ g x) = B.ρ g (f.hom x) for all x ∈ A.

Русский

Для любого гомоморфизма f: A ⟶ B и любого g ∈ G выполняется: f.hom(A.ρ g x) = B.ρ g (f.hom x) для всех x ∈ A.

LaTeX

$$$f.hom (A.ρ g x) = B.\rho g (f.hom x)$$$

Lean4

theorem hom_comm_apply {A B : Rep k G} (f : A ⟶ B) (g : G) (x : A) : f.hom (A.ρ g x) = B.ρ g (f.hom x) :=
  LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp (f.comm g)) x

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