English
The bifunctor map defines a functorial action on graded objects, mapping X and Y to a new graded object via F.
Русский
Двойной функторный отображатель задаёт функториальное действие на градуированные объекты.
LaTeX
$$$mapBifunctorMap F I J:\; GradedObject I C_1 \to GradedObject J C_2 \to GradedObject (I \times J) C_3$$$
Lean4
theorem hexagon_reverse [HasTensor X Y] [HasTensor Y Z] [HasTensor Z X] [HasTensor Z Y] [HasTensor X Z]
[HasTensor (tensorObj X Y) Z] [HasTensor X (tensorObj Y Z)] [HasTensor Z (tensorObj X Y)]
[HasTensor (tensorObj Z X) Y] [HasTensor X (tensorObj Z Y)] [HasTensor (tensorObj X Z) Y]
[HasGoodTensor₁₂Tensor X Y Z] [HasGoodTensorTensor₂₃ X Y Z] [HasGoodTensor₁₂Tensor Z X Y]
[HasGoodTensorTensor₂₃ Z X Y] [HasGoodTensor₁₂Tensor X Z Y] [HasGoodTensorTensor₂₃ X Z Y] :
(associator X Y Z).inv ≫ (braiding (tensorObj X Y) Z).hom ≫ (associator Z X Y).inv =
whiskerLeft X (braiding Y Z).hom ≫ (associator X Z Y).inv ≫ whiskerRight (braiding X Z).hom Y :=
by
ext k i₁ i₂ i₃ h
dsimp [braiding]
conv_lhs =>
rw [ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorObjDesc_assoc, assoc,
← MonoidalCategory.tensorHom_id, BraidedCategory.braiding_naturality_assoc,
BraidedCategory.braiding_tensor_left_hom, assoc, assoc, assoc, assoc, Iso.inv_hom_id_assoc,
MonoidalCategory.id_tensorHom, ← ιTensorObj₃_eq_assoc Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) _ rfl,
ιTensorObj₃_associator_inv, Iso.hom_inv_id_assoc]
conv_rhs =>
rw [ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc, ← MonoidalCategory.id_tensorHom,
MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorObjDesc, categoryOfGradedObjects_id,
MonoidalCategory.id_tensor_comp, assoc, MonoidalCategory.id_tensorHom, MonoidalCategory.id_tensorHom, ←
ιTensorObj₃_eq_assoc X Z Y i₁ i₃ i₂ k (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) (i₂ + i₃) (add_comm _ _),
ιTensorObj₃_associator_inv_assoc,
ιTensorObj₃'_eq X Z Y i₁ i₃ i₂ k (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) _ rfl, assoc, ι_tensorHom,
categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id, ← MonoidalCategory.comp_tensor_id_assoc,
ι_tensorObjDesc, MonoidalCategory.comp_tensor_id, assoc, MonoidalCategory.tensorHom_id,
MonoidalCategory.tensorHom_id, ←
ιTensorObj₃'_eq Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) (i₁ + i₃) (add_comm _ _)]
