English
Compatibility of the primed iota with the tensor of three morphisms: the primed iota composed with tensorHom equals the tensorHom of primed morphisms composed with primed iota.
Русский
Совместимость ιTensorObj3′ с тензором трёх морфизмов: композиция ιTensorObj3′ с tensorHom равна тензорному гомоморфизму по примам morphisms с последующим ιTensorObj3′.
LaTeX
$$$\iotaTensorObj_3' X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ tensorHom (tensorHom f_1 f_2) f_3 j = ((f_1 i_1 ⊗_m f_2 i_2) ⊗_m f_3 i_3) ≫ \iotaTensorObj_3' Y_1 Y_2 Y_3 i_1 i_2 i_3 j h.$$$
Lean4
@[reassoc (attr := simp)]
theorem ιTensorObj₃_associator_inv [HasGoodTensor₁₂Tensor X₁ X₂ X₃] [HasGoodTensorTensor₂₃ X₁ X₂ X₃] (i₁ i₂ i₃ j : I)
(h : i₁ + i₂ + i₃ = j) :
ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (associator X₁ X₂ X₃).inv j =
(α_ _ _ _).inv ≫ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h :=
ι_mapBifunctorAssociator_inv (MonoidalCategory.curriedAssociatorNatIso C) ρ₁₂ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
