English
Under tensor-left, the coequalizer π interacts with colimMap along a parallel pair to produce the same descent as the target h.
Русский
При тензорном левом действии π-коэквалайзер взаимодействует с colimMap вдоль параллельной пары, давая тот же descend к h.
LaTeX
$$$(Z \triangleleft coequalizer.π f g) \;≫\; (PreservesCoequalizer.iso (tensorLeft Z) f g).inv \;≫\; colimMap (parallelPairHom (Z \triangleleft f) (Z \triangleleft g) f' g' p q wf wg) \;≫\; coequalizer.desc h wh = q \;≫\; h.$$$
Lean4
theorem id_tensor_π_preserves_coequalizer_inv_colimMap_desc {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
(p : Z ⊗ X ⟶ X') (q : Z ⊗ Y ⟶ Y') (wf : (Z ◁ f) ≫ q = p ≫ f') (wg : (Z ◁ g) ≫ q = p ≫ g') (h : Y' ⟶ Z')
(wh : f' ≫ h = g' ≫ h) :
(Z ◁ coequalizer.π f g) ≫
(PreservesCoequalizer.iso (tensorLeft Z) f g).inv ≫
colimMap (parallelPairHom (Z ◁ f) (Z ◁ g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
q ≫ h :=
map_π_preserves_coequalizer_inv_colimMap_desc (tensorLeft Z) f g f' g' p q wf wg h wh
