English
In the tensor-right setting with coequalizers, the morphism π interacts with colimMap to yield the descended map equal to h when composed with the inverse of the iso.
Русский
В правой настройке с коэквалайзерами, отображение π взаимодействует с colimMap, давая спуск к h через композицию с инверсией изоморфизма.
LaTeX
$$$(Z \triangleleft coequalizer.π f g) \;≫\; (PreservesCoequalizer.iso (tensorRight Z) f g).inv \;≫\; colimMap (parallelPairHom (f \triangleright Z) (g \triangleright Z) f' g' p q wf wg) \;≫\; coequalizer.desc h wh = q \;≫\; h.$$$
Lean4
theorem π_tensor_id_preserves_coequalizer_inv_colimMap_desc {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
(p : X ⊗ Z ⟶ X') (q : Y ⊗ Z ⟶ Y') (wf : (f ▷ Z) ≫ q = p ≫ f') (wg : (g ▷ Z) ≫ q = p ≫ g') (h : Y' ⟶ Z')
(wh : f' ≫ h = g' ≫ h) :
(coequalizer.π f g ▷ Z) ≫
(PreservesCoequalizer.iso (tensorRight Z) f g).inv ≫
colimMap (parallelPairHom (f ▷ Z) (g ▷ Z) f' g' p q wf wg) ≫ coequalizer.desc h wh =
q ≫ h :=
map_π_preserves_coequalizer_inv_colimMap_desc (tensorRight Z) f g f' g' p q wf wg h wh
