applyAsHom_comm — Mathlib

English

For representations A, B of G and a morphism f: A ⟶ B, the action of g on morphisms commutes: A.applyAsHom g ≫ f = f ≫ B.applyAsHom g for all g ∈ G.

Русский

Для представлений A, B и гомоморфизма f: A ⟶ B выполняется A.applyAsHom g ≫ f = f ≫ B.applyAsHom g для всех g ∈ G.

LaTeX

$$$A.applyAsHom g \; \gg \; f = f \; \gg \; B.applyAsHom g$$$

Lean4

@[reassoc, elementwise]
theorem applyAsHom_comm {A B : Rep k G} (f : A ⟶ B) (g : G) : A.applyAsHom g ≫ f = f ≫ B.applyAsHom g :=
  by
  ext
  simp [hom_comm_apply]

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