English
In a braided Day convolution setting, the usual hexagon coherence condition for the Day convolution braiding holds with reverse orientation. Precisely, for Day convolution F ⊛ G ⊛ H with the associator and braiding coming from the Day convolution, the following equality of natural transformations holds: (associator F G H)^{-1} ∘ (braiding (F ⊛ G) H).hom ∘ (associator H F G)^{-1} = DayConvolution.map(id_F, braiding G H).hom ∘ (associator F H G)^{-1} ∘ DayConvolution.map(braiding F H, id_G).
Русский
В условии braided Day convolution выполняется эквиваленция гексагонального тождества, где преобразования связности образованы в обратном направлении. Пусть F, G, H — деноты (биективные) DayConvolution, тогда композиции, сочетающие ассоциатор и braiding, удовлетворяют заданному равенству, аналогичному обычному гексагону, но с обращением направлений.
LaTeX
$$$(\\alpha_{F,G,H})^{-1} \\;\\circ\\; (\\beta_{(F\\⊛G),H})^{\\mathrm{hom}} \\;\\circ\\; (\\alpha_{H,F,G})^{-1} \;=\; DayConvolution.map(\\mathrm{Id}_F, \\beta_{G,H})^{\\mathrm{hom}} \\;\\circ\\; (\\alpha_{F,H,G})^{-1} \\;\\circ\\; DayConvolution.map(\\beta_{F,H}, \\mathrm{Id}_G)$$$$
Lean4
theorem hexagon_reverse (H : C ⥤ V) [DayConvolution F G] [DayConvolution G H] [DayConvolution F (G ⊛ H)]
[DayConvolution (F ⊛ G) H] [DayConvolution H (F ⊛ G)] [DayConvolution H F] [DayConvolution (H ⊛ F) G]
[DayConvolution H G] [DayConvolution F (H ⊛ G)] [DayConvolution F H] [DayConvolution (F ⊛ H) G] :
(associator F G H).inv ≫ (braiding (F ⊛ G) H).hom ≫ (associator H F G).inv =
(DayConvolution.map (𝟙 F) (braiding G H).hom) ≫
(associator F H G).inv ≫ (DayConvolution.map (braiding F H).hom (𝟙 G)) :=
by
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G ⊛ H) (unit _ _)
apply Functor.hom_ext_of_isLeftKanExtension (F ⊠ (G ⊛ H)) (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F)
ext ⟨x, y, z⟩
dsimp
simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp, Iso.inv_hom_id, associator_inv_unit_unit_assoc,
externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality_assoc, NatTrans.naturality,
unit_app_braiding_hom_app_assoc, BraidedCategory.braiding_tensor_right_hom, Functor.map_comp, Category.assoc,
Iso.map_inv_hom_id, Category.comp_id, BraidedCategory.braiding_naturality_left_assoc,
BraidedCategory.braiding_tensor_left_hom, Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,
unit_app_map_app_assoc, NatTrans.id_app, id_tensorHom]
simp only [← comp_whiskerRight_assoc, ← whiskerLeft_comp_assoc, unit_app_braiding_hom_app]
simp [← Functor.map_comp]
congr 2
rw [← BraidedCategory.hexagon_forward, ← comp_whiskerRight_assoc]
haveI := unit_app_braiding_hom_app F H x z =≫ (H ⊛ F).map (β_ z x).inv
dsimp at this
simp only [Category.assoc, Iso.map_hom_inv_id, Category.comp_id] at this
rw [← this, comp_whiskerRight_assoc]
simp [← Functor.map_comp]
