pushoutIsoUnopPullback_inv_fst — Mathlib

English

In the same setting, the inverse of the canonical pushout–pullback isomorphism composed with the pullback’s first projection equals the opposite of the pushout's left leg.

Русский

В том же окружении обратное изображение канониического изоморфизма пушаут-пуллбак, составленное с проекцией пуллбака на f^{op}, равно противоположной стрелке пушаута влево.

LaTeX

$$$ (\\operatorname{pushoutIsoUnopPullback}(f,g))^{-1} \\!^{op} \\circ \\operatorname{pullback.fst}(f^{op}, g^{op}) = (\\operatorname{pushout.inl}(f,g))^{op} $$$

Lean4

@[simp]
theorem pushoutIsoUnopPullback_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] :
    (pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op = (pushout.inl f g).op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pushoutIsoUnopPullback_inl_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Похожие утверждения