unit_app_braiding_inv_app — Mathlib

English

A variant of the unit-braiding interaction with associativity, expressed as a coherent equality of two compositions.

Русский

Вариант взаимодействия единицы и braiding с ассоциативностью, выраженный как согласованное равенство двух сочетаний.

LaTeX

$$$\text{unit_app_braiding_hom_app_assoc}$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_app_braiding_inv_app (x y : C) :
    (unit G F).app (x, y) ≫ (braiding F G).inv.app (x ⊗ y) =
      (β_ _ _).inv ≫ (unit F G).app (_, _) ≫ (F ⊛ G).map (β_ _ _).inv :=
  by
  change (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _
  simp [braiding, braidingHomCorepresenting, -tensor_obj]

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