β_hom_hom — Mathlib

English

The horizontal component of the braiding on Action agrees with the braiding on the underlying V objects; i.e., the hom morphism of the braiding in Action equals the hom morphism of the braiding in V on the underlying objects.

Русский

Гомоморфизм горизонтальной части браидинга на Action совпадает с браидингом над базовыми объектами V; то есть $ (β_{X,Y})^{\mathrm{hom}} = (β_{X.V,Y.V})^{\mathrm{hom}} $.

LaTeX

$$$ (\beta_{X,Y})^{\mathrm{hom}} = (\beta_{X.V,Y.V})^{\mathrm{hom}} $$$

Lean4

@[simp]
theorem β_hom_hom {X Y : Action V G} : (β_ X Y).hom.hom = (β_ X.V Y.V).hom :=
  rfl

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