forget₂_map_associator_inv — Mathlib

English

Same statement as above reiterated: the forgetful map preserves the inverse of the associator.

Русский

Та же формулировка, повторенная: забывающий функтор сохраняет обратную ассоциатора.

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_inv (X Y Z : QuadraticModuleCat.{u} R) :
    (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).inv =
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv :=
  rfl

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