English
For a mapped parallel pair f,g and given colimMaps, the inverse of the coequalizer iso composes to give the mapped projection equals the target projection via colimMap.
Русский
Для отображения параллельной пары f,g и заданной схемы colimMap обратная сторона коэквалайзера совместно с проекцией даёт соответствие целевой проекции через colimMap.
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) \\\\ = \\\\ q \\;\\circ\\; \\operatorname{coequalizer.\\,π} f' g'. $$$
Lean4
@[reassoc]
theorem map_π_preserves_coequalizer_inv_colimMap {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') :
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) =
q ≫ coequalizer.π f' g' :=
by rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]
