English
Specification of how the four-fold iota tensor object reduces to a whiskered three-fold iota tensor object composed with the outer iota.
Русский
Спецификация того, как четырехкратный iota-тензорный объект сводится к композиции трёхкратного иотаного объекта, обернутого внешним iota.
LaTeX
$$$ιTensorObj_4 X_1 X_2 X_3 X_4 i_1 i_2 i_3 i_4 j h = (_ ◁ ιTensorObj_3 X_2 X_3 X_4 i_2 i_3 i_4 hi) ≫ ιTensorObj X_1 (tensorObj X_2 X_3 X_4) i_1 i_{234} j (by rw [← hi, ← add_assoc, ← add_assoc, h]).$$$
Lean4
theorem pentagon :
tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
(associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
(associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom :=
by
rw [← cancel_epi (associator (tensorObj X₁ X₂) X₃ X₄).inv, ← cancel_epi (associator X₁ X₂ (tensorObj X₃ X₄)).inv,
Iso.inv_hom_id_assoc, Iso.inv_hom_id, ← pentagon_inv_assoc]
simp [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom_assoc]
