English
The morphism ιMapBifunctorMapObj is compatible with the map produced by the Hom action on X and Y.
Русский
Гомоморфизм ιMapBifunctorMapObj совместим с действием по гомоморфизму на X и Y.
LaTeX
$$$ιMapBifunctorMapObj F p X_1 Y_1 i j k h \circ F(f i) = $$$
Lean4
theorem hexagon_forward [HasTensor X Y] [HasTensor Y X] [HasTensor Y Z] [HasTensor Z X] [HasTensor X Z]
[HasTensor (tensorObj X Y) Z] [HasTensor X (tensorObj Y Z)] [HasTensor (tensorObj Y Z) X]
[HasTensor Y (tensorObj Z X)] [HasTensor (tensorObj Y X) Z] [HasTensor Y (tensorObj X Z)]
[HasGoodTensor₁₂Tensor X Y Z] [HasGoodTensorTensor₂₃ X Y Z] [HasGoodTensor₁₂Tensor Y Z X]
[HasGoodTensorTensor₂₃ Y Z X] [HasGoodTensor₁₂Tensor Y X Z] [HasGoodTensorTensor₂₃ Y X Z] :
(associator X Y Z).hom ≫ (braiding X (tensorObj Y Z)).hom ≫ (associator Y Z X).hom =
whiskerRight (braiding X Y).hom Z ≫ (associator Y X Z).hom ≫ whiskerLeft Y (braiding X Z).hom :=
by
ext k i₁ i₂ i₃ h
dsimp [braiding]
conv_lhs =>
rw [ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorObjDesc_assoc, assoc,
← MonoidalCategory.id_tensorHom, BraidedCategory.braiding_naturality_assoc,
BraidedCategory.braiding_tensor_right_hom, assoc, assoc, assoc, assoc, Iso.hom_inv_id_assoc,
MonoidalCategory.tensorHom_id, ←
ιTensorObj₃'_eq_assoc Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h]) _ rfl, ιTensorObj₃'_associator_hom,
Iso.inv_hom_id_assoc]
conv_rhs =>
rw [ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc, ← MonoidalCategory.tensorHom_id,
MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorObjDesc, categoryOfGradedObjects_id,
MonoidalCategory.comp_tensor_id, assoc, MonoidalCategory.tensorHom_id, MonoidalCategory.tensorHom_id, ←
ιTensorObj₃'_eq_assoc Y X Z i₂ i₁ i₃ k (by rw [add_comm i₂ i₁, h]) (i₁ + i₂) (add_comm i₂ i₁),
ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_eq Y X Z i₂ i₁ i₃ k (by rw [add_comm i₂ i₁, h]) _ rfl, assoc,
ι_tensorHom, categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id, ← MonoidalCategory.id_tensorHom, ←
MonoidalCategory.id_tensor_comp_assoc, ι_tensorObjDesc, MonoidalCategory.id_tensor_comp, assoc, ←
MonoidalCategory.id_tensor_comp_assoc, MonoidalCategory.tensorHom_id, MonoidalCategory.id_tensorHom,
MonoidalCategory.whiskerLeft_comp, assoc, ←
ιTensorObj₃_eq Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h]) (i₁ + i₃) (add_comm _ _)]
