English
A technical equality expresses that the three-index injection ιTensorObj₃' is equal to the standard multi-step construction, up to reshuffling of indices as dictated by the associativity isomorphisms.
Русский
Техническое равенство сообщает, что трёхиндексовая инъекция ιTensorObj₃' равна стандартной конструции с учётом ассоциативных перестановок индексов.
LaTeX
$$$ιTensorObj₃' X_1 X_2 X_3 i_1 i_2 i_3 j \;=\; (ιTensorObj X_1 X_2 i_1 i_2 i_1\!\_2 h') \; \rhd\; X_3 i_3 \; \circ \; ιTensorObj (tensorObj X_1 X_2) X_3 i_1\!\_2 i_3 j (by rw[...])$$$
Lean4
@[ext (iff := false)]
theorem tensorObj₃_ext {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A) [H : HasGoodTensorTensor₂₃ X₁ X₂ X₃]
(h :
∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g) :
f = g := by
apply mapBifunctorBifunctor₂₃MapObj_ext (H := H)
intro i₁ i₂ i₃ hi
exact h i₁ i₂ i₃ hi
