English
Given f,g: X → Y with HasCoequalizer, and f', g' : X' → Y' with HasCoequalizer, plus morphisms p: X → X', q: Y → Y' satisfying wf: f ≫ q = p ≫ f' and wg: g ≫ q = p ≫ g', and h: Y' → Z with wh: f' ≫ h = g' ≫ h, then the composite coequalizer π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ coequalizer.desc h wh equals q ≫ h.
Русский
Пусть f,g: X → Y имеют коэквалайзер, а f', g': X' → Y' также. Пусть существуют p: X → X', q: Y → Y' такие, что wf: f ≫ q = p ≫ f' и wg: g ≫ q = p ≫ g', и h: Y' → Z с wh: f' ≫ h = g' ≫ h. Тогда соответствующий композиционный маппинг через colimMap и desc выражает q ≫ h.
LaTeX
$$$ \\pi_{f,g} \\; \\circ \\operatorname{colimMap} (\\operatorname{parallelPairHom} f g f' g' p q wf wg) \\circ \\operatorname{coequalizer}.desc h wh = q \\circ h $$$
Lean4
theorem π_colimMap_desc {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g'] (p : X ⟶ X') (q : Y ⟶ Y')
(wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') (h : Y' ⟶ Z) (wh : f' ≫ h = g' ≫ h) :
coequalizer.π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ coequalizer.desc h wh = q ≫ h := by
rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]
