unit_app_braiding_hom_app — Mathlib

English

A fundamental hexagon axiom for DayConvolution equates two complex compositions of associators and braidings.

Русский

Фундаментальная аксиома гексагональности DayConvolution равенство двух сложных композиций ассоциаторов и braiding.

LaTeX

$$$(\text{associator } F G H).hom ≫ (\text{braiding } F (G \odot H)).hom ≫ (\text{associator } G H F).hom = (\text{DayConvolution.map}(\text{braiding } F G).hom (\mathbf{1}_H)) ≫ (\text{associator } G F H).hom ≫ (\text{DayConvolution.map}(\mathbf{1}_G) (\text{braiding } F H).hom)$$$

Lean4

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

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