English
Let f,g: X → Y have a coequalizer, and suppose G preserves the colimit of the parallel pair f,g and has coequalizers of G.map f and G.map g. Then the image under G of the coequalizer projection, followed by the inverse of the comparison isomorphism, equals the coequalizer projection of the mapped pair.
Русский
Пусть f,g: X → Y имеют коэквалайзер, и пусть G сохраняет колимит пары параллельных стрелок f,g, а также коэквалайзеры для G.map f и G.map g. Тогда образ под действием G проекции коэквалайзера, составленный с обратной стороной сравнения, равен проекции коэквалайзера для пары G.map f, G.map g.
LaTeX
$$$ G\\big(\\operatorname{coequalizer.\\,π}(f,g)\\big) \\;\\circ\\; (\\operatorname{PreservesCoequalizer.iso} G f g)^{-1} \\;=\\; \\operatorname{coequalizer.\\,π}(G\\map f, G\\map g). $$$
Lean4
@[reassoc]
theorem map_π_preserves_coequalizer_inv :
G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g) := by
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id, comp_id]
