English
Let f: X → Y, g: X → Z be as above, with w: f ≫ h = g ≫ k for some h: Y → W and k: Z → W. Then the pushout comparison commutes with G.map applied to the pushout descent; i.e. the naturality square for pushout descents holds under G.
Русский
Пусть f: X → Y, g: X → Z как выше, и пусть существуют h: Y → W и k: Z → W such что f ≫ h = g ≫ k. Тогда диагональ обзора pushout и отображение G сохраняют естественную совместимость между отображением pushout-desc и отображением после применения G.
LaTeX
$$$$ \mathrm{pushoutComparison}(G,f,g) \circ G\big( \mathrm{pushout.desc}_{f,g}(w) \big) = \mathrm{pushout.desc}_{Gf,Gg}(\, \text{by } \text{simp only } [\leftarrow G.map\_comp, w] \,). $$$$
Lean4
@[reassoc (attr := simp)]
theorem pushoutComparison_map_desc (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] {W : C}
{h : Y ⟶ W} {k : Z ⟶ W} (w : f ≫ h = g ≫ k) :
pushoutComparison G f g ≫ G.map (pushout.desc _ _ w) =
pushout.desc (G.map h) (G.map k) (by simp only [← G.map_comp, w]) :=
by ext <;> simp [← G.map_comp]
