English
A simplified variant of hexagon forward coherence for DayConvolution in the braided setting.
Русский
Упрощённая версия коерентности шестигранника для DayConvolution в braided обстановке.
LaTeX
$$$\text{hexagon_forward}^{\;simp}$$$
Lean4
theorem hexagon_forward (H : C ⥤ V) [DayConvolution F G] [DayConvolution G H] [DayConvolution F (G ⊛ H)]
[DayConvolution (F ⊛ G) H] [DayConvolution H F] [DayConvolution G (H ⊛ F)] [DayConvolution (G ⊛ H) F]
[DayConvolution G F] [DayConvolution (G ⊛ F) H] [DayConvolution F H] [DayConvolution G (F ⊛ H)] :
(associator F G H).hom ≫ (braiding F (G ⊛ H)).hom ≫ (associator G H F).hom =
(DayConvolution.map (braiding F G).hom (𝟙 H)) ≫
(associator G F H).hom ≫ (DayConvolution.map (𝟙 G) (braiding F H).hom) :=
by
apply Functor.hom_ext_of_isLeftKanExtension ((F ⊛ G) ⊛ H) (unit _ H)
apply Functor.hom_ext_of_isLeftKanExtension ((F ⊛ G) ⊠ H) (ExternalProduct.extensionUnitLeft (F ⊛ G) (unit F G) H)
ext ⟨⟨x, y⟩, z⟩
dsimp
simp only [whiskerLeft_id, Category.comp_id, associator_hom_unit_unit_assoc, externalProductBifunctor_obj_obj,
tensor_obj, NatTrans.naturality_assoc, NatTrans.naturality, unit_app_braiding_hom_app_assoc,
BraidedCategory.braiding_tensor_left_hom, Functor.map_comp, Category.assoc, Iso.map_hom_inv_id,
BraidedCategory.braiding_naturality_right_assoc, BraidedCategory.braiding_tensor_right_hom,
Iso.map_inv_hom_id_assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, unit_app_map_app_assoc, NatTrans.id_app,
tensorHom_id]
simp only [← comp_whiskerRight_assoc, ← whiskerLeft_comp_assoc, unit_app_braiding_hom_app]
simp only [whiskerLeft_comp, ← Functor.map_comp, Category.assoc, Functor.comp_obj, tensor_obj, comp_whiskerRight,
whiskerRight_comp_unit_app_assoc, NatTrans.naturality_assoc, NatTrans.naturality, associator_hom_unit_unit_assoc,
externalProductBifunctor_obj_obj, unit_app_map_app_assoc, NatTrans.id_app, id_tensorHom]
rw [← BraidedCategory.hexagon_reverse, ← whiskerLeft_comp_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, whiskerLeft_comp_assoc]
simp [← Functor.map_comp]
