op — Mathlib · SciLib

English

Unop version: a pullback in the opposite category corresponds to a pushout in the original category after reversing arrows.

Русский

Обратная версия: пуллбак в противоположной категории соответствует пушауту в исходной после разворота стрелок.

LaTeX

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

Lean4

theorem op (h : IsPullback fst snd f g) : IsPushout g.op f.op snd.op fst.op :=
  IsPushout.of_isColimit
    (IsColimit.ofIsoColimit (Limits.PullbackCone.isLimitEquivIsColimitOp h.flip.cone h.flip.isLimit)
      h.toCommSq.flip.coneOp)

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