English
Let P : Bimod R S, Q : Bimod S T, L : Bimod T U. The inverse followed by the forward associator morphism equals the identity on the underlying object of (P ⊗ Q) ⊗ L.
Русский
Пусть P : Bimod R S, Q : Bimod S T, L : Bimod T U. Обратный ассоциатор после прямого дает тождественный отображение на базовом объекте ((P ⊗ Q) ⊗ L).X.
LaTeX
$$$$ \operatorname{inv}(P,Q,L) \circ \operatorname{hom}(P,Q,L) = \mathrm{id}_{((P \otimes Q) \otimes L).X}. $$$$
Lean4
theorem inv_hom_id : inv P Q L ≫ hom P Q L = 𝟙 _ :=
by
dsimp [hom, homAux, inv, invAux]
apply coequalizer.hom_ext
slice_lhs 1 2 => rw [coequalizer.π_desc]
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
simp only [curriedTensor_obj_map]
slice_lhs 1 3 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
slice_lhs 3 4 => rw [coequalizer.π_desc]
slice_lhs 2 4 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 1 3 => rw [Iso.inv_hom_id_assoc]
dsimp only [TensorBimod.X]
slice_rhs 2 3 => rw [Category.comp_id]
rfl
