unop — Mathlib

English

Unop dual of IsPullback; the isomorphism carries pullbacks to pushouts under opposites.

Русский

Дуальность перехода пуллбека к пушауту через противоположную категорию.

LaTeX

$$$ IsPullback fst snd f g \\Rightarrow IsPushout g^{unop} f^{unop} snd^{unop} fst^{unop} $$$

Lean4

theorem unop {P X Y Z : Cᵒᵖ} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :
    IsPushout g.unop f.unop snd.unop fst.unop :=
  IsPushout.of_isColimit
    (IsColimit.ofIsoColimit (Limits.PullbackCone.isLimitEquivIsColimitUnop h.flip.cone h.flip.isLimit)
      h.toCommSq.flip.coneUnop)

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