ιTensorObj₃'_associator_hom — Mathlib

English

Compatibility of the primed iota with a triple tensor, showing that applying tensorHom to three morphisms corresponds to the primed iota on the target.

Русский

Совместимость ιTensorObj3′ с тройным тензором: применение tensorHom к трём морфизмам эквивалентно применению ι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_hom [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₃).hom j =
      (α_ _ _ _).hom ≫ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h :=
  ι_mapBifunctorAssociator_hom (MonoidalCategory.curriedAssociatorNatIso C) ρ₁₂ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Похожие утверждения