forget₂_map_associator_hom — Mathlib

English

The forgetful functor preserves the inverse of the associator: (forget₂ ...).map (α_ X Y Z).inv = (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv.

Русский

Забывающий функтор сохраняет обратную ассоциатора: (forget₂ ...).map (α_ X Y Z).inv = (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv.

LaTeX

$$$ (forget\_2 (QuadraticModuleCat R) (ModuleCat R)).map (\alpha_ X Y Z).inv = (\alpha_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv $$$

Lean4

theorem forget₂_map_associator_hom (X Y Z : QuadraticModuleCat.{u} R) :
    (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).hom =
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom :=
  rfl

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