English
For graded objects X1, X2, X3 and indices i1, i2, i3, j with h: i1 + i2 + i3 = j and h': i1 + i2 = i12, the canonical associativity morphism ιTensorObj3' satisfies a compatibility relation with the usual tensorial morphisms, namely the displayed equality that rewrites ιTensorObj3' as a composition of ιTensorObj and the evaluation morphisms in a coherent way.
Русский
Для градуированных объектов X1, X2, X3 и индексов i1, i2, i3, j с условиями h: i1+i2+i3=j и h': i1+i2=i12, каноническое отображение ιTensorObj3' удовлетворяет совместимости с обычными тензорными морфизмами: равенство, приводящее ιTensorObj3' к композиции ιTensorObj и соответствующих морфизмов.
LaTeX
$$$$ιTensorObj'_X_1 X_2 X_3 i_1 i_2 i_3 j \, h \, i_{12} \, h' = (ιTensorObj X_1 X_2 i_1 i_2 i_{12} h' \; ▷ \; X_3 i_3) \; ≫ \, ιTensorObj (tensorObj X_1 X_2) X_3 i_{12} i_3 j (by rw[← h', h]).$$$$
Lean4
@[reassoc]
theorem ιTensorObj₃'_eq (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) :
ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
(ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃) ≫ ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j (by rw [← h', h]) :=
by
subst h'
rfl
