English
In any category with pushouts and with pullbacks of opposite arrows, there is a canonical isomorphism between the pushout of f and g and the pullback of f^op and g^op. The right leg of the pushout, composed with this isomorphism, corresponds to the unop of the pullback's second projection.
Русский
В любой категории существуют пушауты и пуллбаки противоположностей; существует каноническое изоморфизм между пушаутом f и g и пуллбаκом f^{op}, g^{op}. Правая стрелка пушаута, композиция с этим изоморфизмом, соответствует развёрнутой второй проекции пуллбака.
LaTeX
$$$ \\operatorname{pushout.inr}(f,g) \\circ (\\operatorname{pushoutIsoUnopPullback}(f,g))^{\\mathrm{hom}} = \\operatorname{unop}(\\operatorname{pullback.snd}(f^{\\mathrm{op}}, g^{\\mathrm{op}})). $$$
Lean4
@[reassoc (attr := simp)]
theorem pushoutIsoUnopPullback_inr_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] :
pushout.inr _ _ ≫ (pushoutIsoUnopPullback f g).hom = (pullback.snd f.op g.op).unop :=
(IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)
