isPushout_iff_op_map_yoneda_isPullback

English

A pushout square is pullback after op and Yoneda mapping: sq.IsPushout iff for all X, (sq.op.map (yoneda.obj X)).IsPullback.

Русский

Pushout-Quadrat после преобразования в Opposite и отображения Yoneda сохраняет свойство pullback: sq.IsPushout эквивалентно тому, что для всех X квадрат (sq.op).map(yoneda.obj X) является pullback.

LaTeX

$$$\\text{IsPushout}(sq) \\iff \\forall X, \\; (sq.\\text{op}.map(\\yoneda.obj X)).IsPullback.$$$

Lean4

theorem isPushout_iff_op_map_yoneda_isPullback : sq.IsPushout ↔ ∀ (X : C), (sq.op.map (yoneda.obj X)).IsPullback :=
  ⟨fun h _ ↦ h.op.map _, fun h ↦
    IsPushout.mk _
      ((sq.pushoutCocone.isColimitYonedaEquiv).symm
        (fun X ↦ IsLimit.ofIsoLimit (h X).isLimit (PullbackCone.ext (Iso.refl _))))⟩

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