English
Inverse associator naturality for ιTensorObj3′ with the associator inverse morphisms.
Русский
Натурализм обратной связности ассоциатора для ιTensorObj3′ с обратным морфизмом ассоциатора.
LaTeX
$$$ιTensorObj_3' X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ (associator X_1 X_2 X_3).inv j = (\alpha_\_\_\_).inv ≫ ιTensorObj_3' X_1 X_2 X_3 i_1 i_2 i_3 j h.$$$
Lean4
@[ext (iff := false)]
theorem tensorObj₄_ext {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A)
[HasGoodTensorTensor₂₃ X₂ X₃ X₄] [H : HasTensor₄ObjExt X₁ X₂ X₃ X₄]
(h :
∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g) :
f = g := by
apply tensorObj_ext
intro i₁ i₂₃₄ h'
apply left_tensor_tensorObj₃_ext
intro i₂ i₃ i₄ h''
have hj : i₁ + i₂ + i₃ + i₄ = j := by simp only [← h', ← h'', add_assoc]
simpa only [assoc, ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j hj i₂₃₄ h''] using h i₁ i₂ i₃ i₄ hj
