English
The inverse component of the associator interacts as the inverse of the hom component in the previous isomorphism.
Русский
Обратная часть ассоциатора ведет себя как обратное к предыдущему гомоморфизму изоморфизма.
LaTeX
$$$\text{(associator)}^{-1} \cdot \text{hom} = \text{inv_hom}$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_mapBifunctorAssociator_inv (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
(mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j =
((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h :=
by
rw [← cancel_mono ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j), assoc, assoc, Iso.inv_hom_id_eval,
comp_id, ι_mapBifunctorAssociator_hom, ← NatTrans.comp_app_assoc, ← NatTrans.comp_app, Iso.inv_hom_id_app,
NatTrans.id_app, NatTrans.id_app, id_comp]
