English
In the same setting, the inverse of the canonical pushout–pullback isomorphism composed with the pullback’s second projection equals the opposite of the pushout's right leg.
Русский
В той же конфигурации обратное отображение канонического изоморфизма пушаут-пуллбак, композиция с проекцией пуллбака на g^{op}, равняется противоположной стрелке пушаута справа.
LaTeX
$$$ (\\operatorname{pushoutIsoUnopPullback}(f,g))^{-1} \\!^{op} \\circ \\operatorname{pullback.snd}(f^{op}, g^{op}) = (\\operatorname{pushout.inr}(f,g))^{op} $$$
Lean4
@[simp]
theorem pushoutIsoUnopPullback_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] :
(pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op = (pushout.inr f g).op :=
by
apply Quiver.Hom.unop_inj
dsimp
rw [← pushoutIsoUnopPullback_inr_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]
