English
In the setting above, the composite of the coequalizer projection, the inverse iso, and the colimMap then the coequalizer.desc recovers the target morphism h.
Русский
В приведённом выше контексте композиция проекции коэквалайзера, обратной стороны изоморфизма и colimMap далее coequalizer.desc восстанавливает целевое гомоморфизм.
LaTeX
$$$ G\\big(\\operatorname{coequalizer.\\,π}(f,g)\\big) \\;\\circ\\; (\\operatorname{PreservesCoequalizer.iso} G f g)^{-1} \\;\\circ\\; \\operatorname{colimMap}(\\text{parallelPairHom}(G.map f)(G.map g) f' g' p q wf wg) \\;\\circ\\; \\operatorname{coequalizer.desc} h wh \\\\ = \\\\ q \\;\\circ\\; \\operatorname{coequalizer.\\,π} f' g'. $$$
Lean4
@[reassoc]
theorem map_π_preserves_coequalizer_inv_colimMap_desc {X' Y' : D} (f' g' : X' ⟶ Y') [HasCoequalizer f' g']
(p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f') (wg : G.map g ≫ q = p ≫ g') {Z' : D} (h : Y' ⟶ Z')
(wh : f' ≫ h = g' ≫ h) :
G.map (coequalizer.π f g) ≫
(PreservesCoequalizer.iso G f g).inv ≫
colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
q ≫ h :=
by
slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]
slice_lhs 2 3 => rw [coequalizer.π_desc]
