op — Mathlib · SciLib

English

If a square is a pushout, then the corresponding square in the opposite category is a pullback.

Русский

Если квадрат является пушаутом, то соответствующий квадрат в противоположной категории является вытянутым/пуллбэком.

LaTeX

$$$\text{If } \text{IsPushout}(f,g,i,j) \text{ then } \text{IsPullback}(j^{\mathrm{op}}, i^{\mathrm{op}}, g^{\mathrm{op}}, f^{\mathrm{op}}).$$$

Lean4

theorem op (h : IsPushout f g inl inr) : IsPullback inr.op inl.op g.op f.op :=
  IsPullback.of_isLimit
    (IsLimit.ofIsoLimit (Limits.PushoutCocone.isColimitEquivIsLimitOp h.flip.cocone h.flip.isColimit)
      h.toCommSq.flip.coconeOp)

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