English
Let f: X → Y and g: X → Z be morphisms in a category C, and suppose pushouts exist for f,g in C and for G.map f, G.map g in D for some functor G: C ⥤ D. Then the canonical map given by the right injection is compatible with the pushout comparison under G; i.e. the composite of the right injection with the pushout comparison equals the image under G of that injection.
Русский
Пусть f: X → Y и g: X → Z — морфизмы в категории C, и существуют соответствующие ассоциации опыта для f,g, а также для их образов G.map f, G.map g в другой категории D, где G: C ⥤ D. Тогда каноническое отображение по правому входу согласовано с переходом через G: композиция pushout.inr f g с pushoutComparison G f g равна G.map (pushout.inr f g).
LaTeX
$$$$\mathrm{pushout.inr}(f,g) \circ \mathrm{pushoutComparison}(G,f,g) = G(\mathrm{pushout.inr}(f,g)).$$$$
Lean4
@[reassoc (attr := simp)]
theorem inr_comp_pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
pushout.inr _ _ ≫ pushoutComparison G f g = G.map (pushout.inr _ _) :=
pushout.inr_desc _ _ _
