English
Equality expressing how ιTensorObj₄ decomposes into a whiskered ιTensorObj₃ and the remaining iota map.
Русский
Согласование разложения ιTensorObj₄ в сочетании с ιTensorObj₃ и оставшейся картой 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
@[reassoc]
theorem pentagon_inv :
tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).inv ≫
(associator X₁ (tensorObj X₂ X₃) X₄).inv ≫ tensorHom (associator X₁ X₂ X₃).inv (𝟙 X₄) =
(associator X₁ X₂ (tensorObj X₃ X₄)).inv ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv :=
by
ext j i₁ i₂ i₃ i₄ h
dsimp only [categoryOfGradedObjects_comp]
conv_lhs =>
rw [ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h _ rfl, assoc, ι_tensorHom_assoc]
dsimp only [categoryOfGradedObjects_id, id_eq, eq_mpr_eq_cast, cast_eq]
rw [id_tensorHom, ← MonoidalCategory.whiskerLeft_comp_assoc, ιTensorObj₃_associator_inv,
ιTensorObj₃'_eq X₂ X₃ X₄ i₂ i₃ i₄ _ rfl _ rfl, MonoidalCategory.whiskerLeft_comp_assoc,
MonoidalCategory.whiskerLeft_comp_assoc, ←
ιTensorObj₃_eq_assoc X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j (by simp only [← add_assoc, h]) _ rfl,
ιTensorObj₃_associator_inv_assoc,
ιTensorObj₃'_eq_assoc X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j (by simp only [← add_assoc, h]) (i₁ + i₂ + i₃)
(by rw [add_assoc]),
ι_tensorHom]
dsimp only [id_eq, eq_mpr_eq_cast, categoryOfGradedObjects_id]
rw [tensorHom_id, whisker_assoc_symm_assoc, Iso.hom_inv_id_assoc, ← MonoidalCategory.comp_whiskerRight_assoc, ←
MonoidalCategory.comp_whiskerRight_assoc, ← ιTensorObj₃_eq X₁ X₂ X₃ i₁ i₂ i₃ _ rfl _ rfl,
ιTensorObj₃_associator_inv, MonoidalCategory.comp_whiskerRight_assoc, MonoidalCategory.pentagon_inv_assoc]
conv_rhs =>
rw [ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ _ _ _ rfl, ιTensorObj₃_eq X₂ X₃ X₄ i₂ i₃ i₄ _ rfl _ rfl, assoc,
MonoidalCategory.whiskerLeft_comp_assoc, ←
ιTensorObj₃_eq_assoc X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j (by rw [← add_assoc, h]) (i₂ + i₃ + i₄)
(by rw [add_assoc]),
ιTensorObj₃_associator_inv_assoc, associator_inv_naturality_right_assoc,
ιTensorObj₃'_eq_assoc X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j (by rw [← add_assoc, h]) _ rfl,
whisker_exchange_assoc, ← ιTensorObj₃_eq_assoc (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h _ rfl,
ιTensorObj₃_associator_inv, whiskerRight_tensor_assoc, Iso.hom_inv_id_assoc,
ιTensorObj₃'_eq (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h _ rfl, ← MonoidalCategory.comp_whiskerRight_assoc, ←
ιTensorObj₃'_eq X₁ X₂ X₃ i₁ i₂ i₃ _ rfl _ rfl]
