English
Let P : Bimod R S, Q : Bimod S T, L : Bimod T U. The associator between these bimodules has an inverse, and their composition is 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{hom}(P,Q,L) \circ \operatorname{inv}(P,Q,L) = \mathrm{id}_{((P \otimes Q) \otimes L).X}. $$$$
Lean4
theorem hom_inv_id : hom P Q L ≫ inv P Q L = 𝟙 _ :=
by
dsimp [hom, homAux, inv, invAux]
apply coequalizer.hom_ext
slice_lhs 1 2 => rw [coequalizer.π_desc]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
simp only [Functor.flip_obj_map, curriedTensor_map_app]
slice_lhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 3 4 => rw [coequalizer.π_desc]
slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
slice_lhs 1 3 => rw [Iso.hom_inv_id_assoc]
dsimp only [TensorBimod.X]
slice_rhs 2 3 => rw [Category.comp_id]
rfl
